Proof of basic defining property of remove_singleton

----> UNIT CONFLICT at  47.26 sec ----> 3570 [binary,3569.1,8.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.
8 [reference] x=x.
21 [reference] p1 x=p2 x |eq x =p2.
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))))).
80 [assumption to refute] p.
81 [assumption to refute] badset bad=p1.
82 [assumption to refute] bad!=bad1.
83 [assumption to refute] -p|remove_singleton pair(badset,k(bad1)) bad !=p1.
106 [ur,83,80,demod,79,6,1,4,1,4,2,6,1,4,3,1,6,1,4,1,4,6,1,4,1,4,5] eq pair(pair(p1,p2),pair(badset bad,eq pair(bad1,bad)))!=p1.
138 [para_into,106.1.1.2.2.2,21.2.1,demod,2,3] eq pair(pair(p1,p2),pair(badset bad,p2))!=p1|bad1=bad.
2711,2710 [para_into,138.1.1.2.1.1,81.1.2,demod,7,unit_del,8] bad1=bad.
3569 [back_demod,82,demod,2711] bad!=bad.
3570 [binary,3569.1,8.1] $F.