Proof of remove_singleton pair(xset,k(x)) x = p2.

----> UNIT CONFLICT at   1.51 sec ----> 184 [binary,182.1,19.1] $F.

Length of proof is 4.  Level of proof is 4.

Proof

1 [reference] k(x) y=x.
2 [reference] p1 pair(x,y)=x.
3 [reference] p2 pair(x,y)=y.
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).
7 [reference] eq pair(x,x)=p1.
19 [reference] p2!=p1.
21 [reference] p1 x=p2 x |eq x =p2.
53 [reference] pair(x1,y1)!=pair(x2,y2)|y1=y2.
79 [reference] remove_singleton=abst k(abst k(eq)) pair(k(k(pair(p1,p2))),pair(p1,abst k(abst k(eq)) pair(p2,k(pair(p1,p2))))).
81 [reference] xset x=p1|remove_singleton pair(xset,y) x =p2.
82 [assumption to refute] p.
83 [assumption to refute] -p|remove_singleton pair(badset,k(bad)) bad !=p2.
95,94 [hyper,83,82,81] badset bad=p1.
104 [ur,83,82,demod,79,6,1,4,1,4,2,6,1,4,3,1,6,1,4,1,4,95,6,1,4,1,4,5,7] eq pair(pair(p1,p2),pair(p1,p1))!=p2.
175 [hyper,104,21,demod,2,3] pair(p1,p2)=pair(p1,p1).
182 [hyper,175,53] p2=p1.
184 [binary,182.1,19.1] $F.