prove_imp: tm form -> tm form -> type = 
  [A][B] pf (A imp B).

%clause
prove_imp1: prove_imp A true =
  imp_i [p1: pf A] true_i.

%clause
prove_imp2: prove_imp A A = 
  imp_i [p1: pf A] p1.

%clause
prove_imp3: prove_imp A (B and C) <-
   prove_imp A B <-
   prove_imp A C =
 [p1: prove_imp A C]
 [p2: prove_imp A B]
 imp_i [p3: pf A]
 and_i (imp_e p2 p3) (imp_e p1 p3).

%clause
prove_imp4: prove_imp (A and B) C <-
     prove_imp A C =
 [p1: prove_imp A C]
 imp_i [p2: pf (A and B)] 
 imp_e p1 (and_e1 p2).

%clause
prove_imp5: prove_imp (A and B) C <-
     prove_imp B C =
 [p1: prove_imp B C]
 imp_i [p2: pf (A and B)] 
 imp_e p1 (and_e2 p2).

f: rational -> tm form.

%solve P : prove_imp ((f 3 and f 1) and (f 2 and f 4)) 
                     (f 1).

%solve P : prove_imp ((f 3 and f 1) and (f 2 and f 4)) 
                     (f 1 and f 2 and f 3 and f 4 and true).