Proof of key lemma on closure and remove_singleton

----> UNIT CONFLICT at   4.52 sec ----> 1524 [binary,1523.1,23.1] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).

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

Proof

23 [reference] p2!=p1.
50 [reference] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1.
77 [reference] closedunder pair(closure pair(xs,xf),xf)=p1.
79 [reference] closure x y=p1|closure x y =p2.
84 [reference] xset x=p1|remove_singleton pair(xset,y) x =p2.
86 [reference] closedunder pair(xs,xf)=p2|closedunder pair(remove_singleton pair(xs,k(x)),xf) =p1|xf notclosed(remove_singleton pair(xs,k(x)),xf) =x.
97 [assumption to refute] closure pair(bads,badf) x!=p1|badf x !=bad|$ans(x).
98 [assumption to refute] closedunder pair(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)!=p1.
100 [hyper,98,86] closedunder pair(closure pair(bads,badf),badf)=p2|badf notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf) =bad.
103 [hyper,98,50] remove_singleton pair(closure pair(bads,badf),k(bad)) notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)=p1.
366,365 [para_into,103.1.1,84.2.1,unit_del,23] closure pair(bads,badf) notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)=p1.
377 [hyper,100,97,79,demod,366,unit_del,23] closedunder pair(closure pair(bads,badf),badf)=p2|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).
1523 [para_into,377.1.1,77.1.1,flip.1] p2=p1|$ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).
1524 [binary,1523.1,23.1] $ans(notclosed(remove_singleton pair(closure pair(bads,badf),k(bad)),badf)).