Proof that the closure is the smallest such set

----> UNIT CONFLICT at   0.23 sec ----> 89 [binary,87.1,80.1] $F.

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

Proof

5 [reference] pair(p1 x,p2 x)=x.
74 [reference] closedunder pair(x,xf)=p2|subset pair(xs,x) =p2|subset pair(closure pair(xs,xf),x) =p1.
78 [assumption to refute] closedunder pair(bad2,p2 bad1)!=p2.
79 [assumption to refute] subset pair(p1 bad1,bad2)!=p2.
80 [assumption to refute] subset pair(closure bad1,bad2)!=p1.
87 [ur,79,74,78,demod,5] subset pair(closure bad1,bad2)=p1.
89 [binary,87.1,80.1] $F.