Proof of important lemma on closedunder and remove_singleton

----> UNIT CONFLICT at   1.33 sec ----> 335 [binary,334.1,8.1] $ans(notclosed(remove_singleton pair(bads,k(bad)),badf)).

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

Proof

8 [reference] x=x.
19 [reference] p2!=p1.
45 [reference] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1.
46 [reference] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1.
47 [reference] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1.
79 [reference] xset x!=p1|x=x1|remove_singleton pair(xset,k(x1)) x =p1.
80 [reference] xset x=p1|remove_singleton pair(xset,y) x =p2.
82 [assumption to refute] closedunder pair(bads,badf)!=p2.
83 [assumption to refute] badf x!=bad|$ans(x).
84 [assumption to refute] closedunder pair(remove_singleton pair(bads,k(bad)),badf)!=p1.
95 [hyper,84,46] remove_singleton pair(bads,k(bad)) notclosed(remove_singleton pair(bads,k(bad)),badf)=p1.
107 [neg_hyper,84,47] remove_singleton pair(bads,k(bad)) (badf notclosed(remove_singleton pair(bads,k(bad)),badf))!=p1.
156 [para_into,95.1.1,80.2.1,unit_del,19] bads notclosed(remove_singleton pair(bads,k(bad)),badf)=p1.
316,315 [ur,156,45,82] bads (badf notclosed(remove_singleton pair(bads,k(bad)),badf))=p1.
334 [neg_hyper,107,79,83,demod,316] p1!=p1|$ans(notclosed(remove_singleton pair(bads,k(bad)),badf)).
335 [binary,334.1,8.1] $ans(notclosed(remove_singleton pair(bads,k(bad)),badf)).