Proof that the closure contains the set

----> UNIT CONFLICT at   1.18 sec ----> 650 [binary,649.1,8.1] $F.

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

Proof

8 [reference] x=x.
13 [reference] pair(p1 x,p2 x)=x.
72 [reference] subset pair(xs,closure pair(xs,xf))=p1.
76 [assumption to refute] subset pair(p1 bad,closure bad)!=p1.
104 [para_into,76.1.2,72.1.2] subset pair(p1 bad,closure bad)!=subset pair(x,closure pair(x,y)).
649 [para_into,104.1.2.2.2.2,13.1.1] subset pair(p1 bad,closure bad)!=subset pair(p1 x,closure x).
650 [binary,649.1,8.1] $F.