Proof that if x is in pushset then push x is in pushset.

Proof that if `x` is in `pushset` then `push x` is in `pushset`.

----> UNIT CONFLICT at   2.38 sec ----> 615 [binary,613.1,23.1] $F.

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

Proof



12 [reference] x=x.
23 [reference] p2!=p1.
49 [reference] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1.
77 [reference] closedunder pair(closure pair(xs,xf),xf)=p1.
79 [reference] closure x y=p1|closure x y =p2.
84 [reference] closure pair(notp1 charq,setof) x=p2|push x =setof x.
88 [assumption to refute] closure pair(notp1 charq,setof) bad!=p2.
89 [assumption to refute] closure pair(notp1 charq,setof) (push bad)!=p1.
92,91 [hyper,88,79] closure pair(notp1 charq,setof) bad=p1.
98 [hyper,89,79] closure pair(notp1 charq,setof) (push bad)=p2.
137 [para_into,98.1.1.2,84.2.1,demod,92,unit_del,23] closure pair(notp1 charq,setof) (setof bad)=p2.
384 [para_into,137.1.1,49.3.1,demod,92,unit_del,23,12] closedunder pair(closure pair(notp1 charq,setof),setof)=p2.
613 [para_into,384.1.1,77.1.1,flip.1] p2=p1.
615 [binary,613.1,23.1] $F.