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

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

----> UNIT CONFLICT at   0.29 sec ----> 104 [binary,103.1,12.1] $F.

Length of proof is 3.  Level of proof is 2.

Proof



12 [reference] x=x.
79 [reference] closure x y=p1|closure x y =p2.
83 [reference] closure pair(notp1 charq,setof) x=p1|push x =x.
89 [assumption to refute] closure pair(notp1 charq,setof) bad!=p1.
90 [assumption to refute] closure pair(notp1 charq,setof) (push bad)!=p2.
92,91 [hyper,89,83] push bad=bad.
94,93 [hyper,89,79] closure pair(notp1 charq,setof) bad=p2.
103 [back_demod,90,demod,92,94] p2!=p2.
104 [binary,103.1,12.1] $F.