Proof that the function push always agrees with the identity function or with setof

Proof that the function `push` always agrees with the identity function or with `setof`

----> UNIT CONFLICT at   0.26 sec ----> 128 [binary,126.1,23.1] $F.

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

Proof



23 [reference] p2!=p1.
83 [reference] closure pair(notp1 charq,setof) x=p1|push x =x.
84 [reference] closure pair(notp1 charq,setof) x=p2|push x =setof x.
87 [assumption to refute] push bad!=bad.
88 [assumption to refute] push bad!=setof bad.
90,89 [hyper,87,83] closure pair(notp1 charq,setof) bad=p1.
126 [hyper,88,84,demod,90,flip.1] p2=p1.
128 [binary,126.1,23.1] $F.