prove_imp: {a: tm form}{b: tm form} pf (a imp b) -> type.

prove_imp1: prove_imp A true (imp_i [x] true_i).

prove_imp2: prove_imp A A (imp_i [p1] p1).

prove_imp3: prove_imp A (B and C) (imp_i[p] and_i (imp_e P1 p) (imp_e P2 p)) <-
      prove_imp A B P1 <-
      prove_imp A C P2.

prove_imp4: prove_imp (A and B) C (hole (A and B imp C)) <-
      prove_imp A C P.

prove_imp5: prove_imp (A and B) C (hole (A and B imp C)) <-
      prove_imp B C P.

f: rational -> tm form.

%define p22 = P
%solve q22 : prove_imp ((f 3 and f 1) and (f 2 and f 4))   (f 1)  P.

%define p23 = P
%solve q23 : 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)  P.