%%% Add the theorems and their proofs in this file.

p1_a: ...
p1_b: ...
p1_c: ...


exists_uniq_i: 
  pf (A X) -> 
    pf (forall [Y] A Y imp eq X Y) ->
       pf (exists_uniq A) = 

exists_uniq_i1: 
  pf (A X) -> 
   ({Y} pf (A Y) -> pf (eq X Y)) ->
       pf (exists_uniq A) =

exists_uniq_e: 
 pf (exists_uniq A) ->
  ({X:tm T} 
    pf (A X) ->
     pf (forall [Y] A Y imp eq X Y) -> 
      pf B) ->
   pf B =

exists_uniq_e1: 
  pf (exists_uniq A) ->
   ({X:tm T} pf (A X) -> pf B) -> pf B =

exists_uniq_e2: 
   pf (exists_uniq A) ->
     pf (A X) -> pf (A Y) -> pf (eq X Y) =

lemma4: pf (eq (plus (plus C B) (times (pred A) B)) (plus C (times A B))) =
 cut bighole
     [p3: pf (eq (times (pred A) B) (plus (times B A) (times B (neg one))))]
 cut bighole
     [p4: pf (eq (plus (times (pred A) B) B)
                 (plus (plus (times B A) (times B (neg one))) B))]
 cut bighole
     [p5: pf (eq (plus (times (pred A) B) B)
                 (plus (times B A) (plus (times B (neg one)) B)))]
 cut bighole
     [p6: pf (eq (times B (neg one)) (neg B))]
 cut bighole
     [p7: pf (eq (plus (times B (neg one)) B) zero)]
 cut bighole
     [p8: pf (eq (plus (times (pred A) B) B) (times B A))]
 cut bighole
     [p9: pf (eq (plus (times (pred A) B) B) (times A B))]
 cut bighole
     [p10: pf (eq (plus B (times (pred A) B)) (times A B))]
 cut bighole
     [p11: pf (eq (plus C (plus B (times (pred A) B))) (plus C (times A B)))]
 bighole.