Proof of a(x,y) = p1 | a(a(isp1,x),y) = p2.

----> UNIT CONFLICT at   0.11 sec ----> 56 [binary,54.1,22.1] $F.

Length of proof is 2.  Level of proof is 2.

Proof

1 [reference] k(x) y=x.
4 [reference] pair(x,y) z=pair(x z,y z).
5 [reference] pair(p1 x,p2 x)=x.
6 [reference] abst x y z=x k(z) (y z).
16 [reference] x=y|eq pair(x,y) =p2.
19 [reference] isp1=abst k(abst k(eq)) pair(k(k(p1)),pair(p1,p2)).
21 [assumption to refute] p.
22 [assumption to refute] bad1 bad2!=p1.
23 [assumption to refute] -p|isp1 bad1 bad2 !=p2.
29 [ur,23,21,demod,19,6,1,4,1,4,5,6,1,4,1] eq pair(p1,bad1 bad2)!=p2.
54 [ur,29,16,flip.1] bad1 bad2=p1.
56 [binary,54.1,22.1] $F.