%%% Useful lemmas
bighole : pf A.

cut : pf A -> (pf A -> pf B) -> pf B =
 [p1 : pf A]
 [p2 : pf A -> pf B]
  imp_e (imp_i p2) p1.

%%% Complete the proofs by filling in the ...

%%% Problem (3a)
mt : pf (A imp B) -> pf (not B) -> pf (not A) =
 [p1 : pf (A imp B)]
 [p2 : pf (not B)]
  ...

not_not_i : pf A -> pf (not (not A)) = ...

raa : (pf (not A) -> pf false) -> pf A = ...

lem : pf (A or not A) =
 (not_not_e ...

% Exercise 2.5.4, page 126 of H&R

ex2_5_4_a : ...

ex2_5_4_b : ...

ex2_5_4_c : ...

% Exercise 2.5.6, page 126 of H&R

ex2_5_6_a : ...

ex2_5_6_b : ...

ex2_5_6_c : ...

ex2_5_6_d : ...


% Exercise 2.5.9, page 127 of H&R

ex2_5_9_a : ...

ex2_5_9_b : ...

ex2_5_9_c : ...

ex2_5_9_d : ...

ex2_5_9_e : ...

ex2_5_9_f : ...

ex2_5_9_g : ...

ex2_5_9_h : ...

ex2_5_9_i : ...