Proof that pushset (push x) = pushset x

Proof that `pushset (push x) = pushset x`

-----> EMPTY CLAUSE at   0.33 sec ----> 139 [para_into,90.1.2,88.2.1,demod,131,1
31,unit_del,12,23] $F.

Length of proof is 1.  Level of proof is 1.

Proof



12 [reference] x=x.
23 [reference] p2!=p1.
83 [reference] closure pair(notp1 charq,setof) x=p1|push x =x.
88 [reference] closure pair(notp1 charq,setof) x=p2|closure pair(notp1 charq,setof) (push x) =p1.
90 [assumption to refute] closure pair(notp1 charq,setof) bad!=closure pair(notp1 charq,setof) (push bad).
131,130 [para_into,90.1.2.2,83.2.1,unit_del,12] closure pair(notp1 charq,setof) bad=p1.
139 [para_into,90.1.2,88.2.1,demod,131,131,unit_del,12,23] $F.