module let.
 
accumulate letSig.

accumulate basiclem.

def_lemma add_under_forall 
  (Proof\ pi A\ pi B\ pi Q\ pi B'\
     (Proof Q B' proves (forall Z\ A Z imp B Z) :-
        assume (forall Z\ A Z imp B' Z),
        pi Z\ (assume (A Z) => assume (B' Z) => Q Z proves B Z)))
  (Q\B'\ just_because).

def_lemma add_under_forall_gen 
  (Proof\ pi B\ pi Q\ pi B'\ pi R\ pi R'\ pi P\
     (Proof P Q R' B' proves (forall Z\ eq Z R imp B Z) :-
        assume (forall Z\ eq Z R' imp B' Z),
        P proves eq R' R,
        pi Z\ (assume (eq Z R) => assume (B' Z) => Q Z proves B Z)))
  (P\Q\R'\B'\ just_because).

def_lemma add_under_forall2 
  (Proof\ pi R\ pi B\ pi C\ pi Q\ (
    Proof Q C R  proves B :-
        assume (forall r\ ((eq r R) imp (C r))),
        (assume (C R) => Q proves B)))
  (Q\C\R\ just_because).

def_lemma add_under_forall3
  (Proof\ pi X\ pi R\ pi C\ pi B\ pi Q\ (
      Proof Q R C X proves B :-
         assume (eq X R), assume (forall r\ (eq r R imp C r)), 
         (assume (C X) => Q proves B)))
  (Q\R\C\X\ just_because).

def_lemma merge_formulas_and1
  (Proof\ pi A\ pi B\ pi C\ 
     (Proof proves (A and B) :-
          assume (A and (B and C))))
  (just_because).

def_lemma merge_formulas_and2
  (Proof\ pi A\ pi B\ pi C\ pi A'\ pi P\
     (Proof P A proves (A' and C) :-
          assume (A and (B and C)),
          assume A => P proves A'))
  (P\A\ just_because).

def_lemma merge_formulas_lemma1
  (Proof\ pi P\ pi A\ pi B\ pi A'\ pi C\
      (Proof P proves (A and B) and (A' and C) :-
          assume (A and (B and C)),
          assume A => P proves A'))
  (P\ just_because).

def_lemma merge_formulas_lemma2
  (Proof\ pi P\ pi C\ pi A\ pi R\ pi B\
      (Proof P C proves (forall r\ ((eq r R) imp (A r))) 
                        and (forall r\ ((eq r R) imp (B r))) :-
          assume (forall r\ ((eq r R) imp (C r))),
          pi r\ assume (C r) => assume (eq r R) => P r proves A r and B r))
  (P\C\ just_because).

def_lemma merge_formulas_lemma3
  (Proof\ pi P\ pi C\ pi A\ pi R\ pi B\
      (Proof P C proves (forall r\ ((eq r R) imp (A r))) and B :-
          assume (forall r\ ((eq r R) imp (C r))),
          pi r\ assume (C r) => assume (eq r R) => P r proves A r and B))
  (P\C\ just_because).

def_lemma merge_formulas_lemma4 
  (Proof\ pi P\ pi C\ pi A\ pi R\ pi B\
      (Proof P C proves A and (forall r\ ((eq r R) imp (B r))) :-
          assume (forall r\ ((eq r R) imp (C r))),
          pi r\ assume (C r) => assume (eq r R) => P r proves A and B r))
  (P\C\ just_because).


def_lemma cut_and_elim
  (Proof\ pi P\ pi Q\ pi C\ pi A\ pi B\
   (Proof P Q A B proves C :-
    P proves (A and B), assume A => assume B => Q proves C))
   (P\ Q\ A\ B\ just_because).

def_lemma sink_conj_lemma1
  (Proof\ pi A\ pi R\ pi C\ pi D\ pi Q\
       (Proof Q C proves (A and (forall r\ eq r R imp D r)) :-
            assume (forall r\ eq r R imp C r),
            pi r\ (assume (eq r R) =>
			  assume (C r) => Q r proves (A and (D r)))))
  (Q\ C\ just_because).

def_lemma sink_conj_lemma2
  (Proof\ pi Q\ pi A\ pi D\ pi A'\
       (Proof Q A' proves ((eq allocptr A) and D) :-
            assume ((eq allocptr A') and D),
            Q proves (eq A' A)))
  (Q\ A'\ just_because).