Proof of piecewise characterization of push, case 2

-----> EMPTY CLAUSE at   2.17 sec ----> 264 [para_into,88.1.1.1.2.2.1,79.1.1,demod,7,2,unit_del,12,86] $F.

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

Proof

1 [reference] k(x) y=x.
2 [reference] p1 pair(x,y)=x.
4 [reference] pair(x,y) z=pair(x z,y z).
5 [reference] pair(p1 x,p2 x)=x.
6 [reference] abst x y z=x k(z) (y z).
7 [reference] eq pair(x,x)=p1.
12 [reference] x=x.
55 [reference] abst k(x) k(y)=k(x y).
79 [reference] closure x y=p1|closure x y =p2.
83 [reference] push=abst (abst k(eq) pair(k(k(p1)),abst k(closure pair(notp1 charq,setof)))) pair(setof,pair(p1,p2)).
85 [assumption to refute] p.
86 [assumption to refute] closure pair(notp1 charq,setof) bad!=p2.
87 [assumption to refute] -p|push bad !=setof bad.
88 [ur,87,85,demod,83,6,6,1,4,1,55,4,4,5] eq pair(k(p1),k(closure pair(notp1 charq,setof) bad)) pair(setof bad,bad)!=setof bad.
264 [para_into,88.1.1.1.2.2.1,79.1.1,demod,7,2,unit_del,12,86] $F.