/\ = [a][b] set_intersection @ a @ b.

%infix right 20 /\.

prove_sub: tm (set T) -> tm (set T) -> type = [A][B] pf (subset @ A @ B).

fact: tm (set T) -> tm (set T) -> type = [A][B] pf (subset @ A @ B).

finish: tm (set T) -> tm (set T) -> type = [A][B] pf (subset @ A @ B).

make_facts: tm (set T) -> tm (set T) -> tm (set T) -> type =
   [A][B][C] pf (subset @ A @ B imp subset @ A @ C).


%clause
prove_sub1: prove_sub A C <-
             make_facts A A C =
 [p1: pf (subset @ A @ A imp subset @ A @ C)]
 imp_e p1 subset_refl.
 
%clause
make_facts0: make_facts A0 ((B /\ C) /\ D) E <-
               make_facts A0 (B /\ (C /\ D)) E =
 [p1: pf (subset @ A0 @ (B /\ (C /\ D)) imp subset @ A0 @ E)]
 imp_i [p2: pf (subset @ A0 @ ((B /\ C) /\ D))]
 cut (subset_i [x][p3: pf (((B /\ C) /\ D) @ x)]
      set_intersection_i 
       (set_intersection_e1 (set_intersection_e1 p3))
       (set_intersection_i (set_intersection_e2 (set_intersection_e1 p3))
        (set_intersection_e2 p3)))
       [p10: pf (subset @ ((B /\ C) /\ D) @ (B /\ (C /\ D)))]
 imp_e p1 (subset_trans p2 p10).

%clause
make_facts1: make_facts A0 (A /\ B) C <-
               (fact A0 A -> make_facts A0 B C) =
 [p1: pf (subset @ A0 @ A) -> pf (subset @ A0 @ B imp subset @ A0 @ C)]
 imp_i [p2: pf (subset @ A0 @ (A /\ B))]
 cut (subset_i [x][p3: pf (A0 @ x)] set_intersection_e1 (subset_e p2 p3))
       [p4: pf (subset @ A0 @ A)]
 cut (subset_i [x][p5: pf (A0 @ x)] set_intersection_e2 (subset_e p2 p5))
       [p6: pf (subset @ A0 @ B)]
 imp_e (p1 p4) p6.

%clause
make_facts2: make_facts A0 A C <-
               (fact A0 A -> finish A0 C) =
 [p1: pf (subset @ A0 @ A) -> pf (subset @ A0 @ C)]
 imp_i [p2: pf (subset @ A0 @ A)]
 p1 p2.

%clause
finish1: finish A0 (B /\ C) <-
              finish A0 B <-
              finish A0 C =
 [p1: pf (subset @ A0 @ C)]
 [p2: pf (subset @ A0 @ B)]
 subset_i [x][p3: pf (A0 @ x)]
 set_intersection_i (subset_e p2 p3) (subset_e p1 p3).

%clause
finish2: finish A0 B <- fact A0 B = [p1] cut p1 [_] p1.

f: rational -> tm (set num).

%solve P : prove_sub ((f 3 /\ f 1) /\ (f 2 /\ f 4))
                     (f 1).

%solve P : prove_sub ((f 3 /\ f 1) /\ (f 2 /\ f 4)) 
                     (f 1 /\ f 2 /\ f 3 /\ f 4).