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

fact: tm form -> type =
  [A] pf A.

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

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

%clause
prove_imp1: prove_imp A C <-
             make_facts A A C =
  [p1: pf (A imp A imp C)]
  imp_i [p2: pf A] imp2_e p1 p2 p2.

%clause
make_facts0: make_facts A0 ((B and C) and D) E <-
               make_facts A0 (B and (C and D)) E =
  [p1: pf (A0 imp (B and C and D) imp E)]
  imp2_i [p2: pf A0]
         [p3: pf ((B and C) and D)]
  and_l p3
        [p4: pf (B and C)]
        [p5: pf D]
  cut (and_i (and_e1 p4) (and_i (and_e2 p4) p5))
        [p6: pf (B and (C and D))]
  imp2_e p1 p2 p6.

%clause
make_facts1: make_facts A0 (A and B) C <-
               (fact A -> make_facts A0 B C) =
 [p1: pf A -> pf (A0 imp B imp C)]
 cut (imp_i p1) [_]
 imp2_i [p2: pf A0]
        [p3: pf (A and B)]
 imp2_e (p1 (and_e1 p3)) p2 (and_e2 p3).

%clause
make_facts2: make_facts A0 A C <-
               (fact A -> finish A0 C) =
 [p1: pf A -> pf (A0 imp C)]
 cut (imp_i p1) [_]
 imp2_i [p2: pf A0]
        [p3: pf A]
 imp_e (p1 p3) p2.

%clause
finish1: finish A0 (B and C) <-
              finish A0 B <-
              finish A0 C =
 [p1: pf (A0 imp C)]
 [p2: pf (A0 imp B)]
 imp_i [p3: pf A0]
 and_i (imp_e p2 p3) (imp_e p1 p3).

%clause
finish2: finish A0 B <- fact B =
  [p1: pf B]
  imp_i [p2: pf A0] p1.

%clause
finish3: finish A0 true =
  imp_i [p2: pf A0] true_i.

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).