%%% 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) ())) --*-> ?