%%% Assignment 4
%%% Out: Monday 1st Oct
%%% Due: Monday 8th Oct
annotated proof p1 : (A | ~ A) => ((A => B) => A) => A;
annotated proof p2 :~A | ~B => ~(A & B);
term M : (A => C) => ((B => C) => (A | B => C));
term N : (A => B => C) => (A => B) => A => C;
term O : (A => B => C) => B => A => C;
term P : ((A | B) => C) => (A => C) & (B => C);
% Hand-in on paper :
% Show the reduction sequence for
% N (fn x => fn y => y) (fn x => x) (fn x => fn y => x) --*-> ?
% Show the reduction sequence for
% M (fn x => x) ((fn x => inl x) ((fn x => fn y => x )(fn x => fn y => x y) ())) --*-> ?