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

----> UNIT CONFLICT at   0.16 sec ----> 107 [binary,105.1,34.1] $F.

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

Proof

5 [reference] pair(p1 x,p2 x)=x.
32 [reference] setof xf pair(x,xf x)=p1.
34 [assumption to refute] setof badf badp!=p1.
35 [assumption to refute] p2 badp=badf (p1 badp).
105 [para_from,35.1.2,32.1.1.2.2,demod,5] setof badf badp=p1.
107 [binary,105.1,34.1] $F.