%%% Assignment 2
%%% Out: Thursday Sep 14
%%% Due: Thursday Sep 21
%%%
%%% see ass2-extra.req for extra credit problems
%%% see ass1.tut for model solutions for Assignment 1

annotated proof OrIL : A => A | B;

annotated proof Trans : (A => B) => (B => C) => (A => C);

annotated proof FE : A & ~ A => C;

term MT : (A => B) => (~B => ~A);

% from Assignment 1
annotated proof L19a : ((A | B) => C) => (A => C) & (B => C);
term L19b : (A => C) & (B => C) => ((A | B) => C);

proof L18a : (A | C) & (B => C) => ((A => B) => C);
term L18a : (A | C) & (B => C) => ((A => B) => C);

proof XM : ~~(A | ~A);
term XM : ~~(A | ~A);