Proof of a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2.

Proof of `a(p2,xy) = a(xf,a(p1,xy)) | a(a(setof,xf),xy) = p2.`

----> UNIT CONFLICT at   0.34 sec ----> 226 [binary,224.1,35.1] $F.

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

Proof



5 [reference] pair(p1 x,p2 x)=x.
33 [reference] setof xf pair(x,y)=p2|xf x =y.
35 [assumption to refute] setof badf badp!=p2.
36 [assumption to refute] p2 badp!=badf (p1 badp).
38,37 [ur,35,33] setof (setof badf) pair(badp,p2)=p2.
181 [para_from,37.1.2,36.1.1.1,demod,38,flip.1] badf (p1 badp)!=p2 badp.
224 [ur,181,33,demod,5] setof badf badp=p2.
226 [binary,224.1,35.1] $F.