%%% Useful lemmas
bighole : pf A.
hole: {A} 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.

%%% The derived rules of page 31 that we treat as axioms for now.
%%% Make use of them in the proofs below if you like.
mt : pf (A imp B) -> pf (not B) -> pf (not A).

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

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

lem : pf (A or not A).

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

%%% Problem (4a)
p4a : pf ((A and B) and C) -> pf (D and E) -> pf (B and D) =
 [p1 : pf ((A and B) and C)]
 [p2 : pf (D and E)]
  ...

%%% Problem (4b) - Only the forward direction
p4b : pf (A imp B) -> pf (not A or B) =
 [p1 : pf (A imp B)]
  ...

%%% Problem (4c) - Only the forward direction
p4c : pf (A imp B) -> pf (not B imp not A) =
 [p1 : pf (A imp B)]
  ...

%%% Problem (4d) - prove Example 1.13 from page 17 of Huth and Ryan.
p4d: ...