Proof that the closure is closed

----> UNIT CONFLICT at   2.09 sec ----> 885 [binary,884.1,249.1] $F.

Length of proof is 6.  Level of proof is 4.

Proof

13 [reference] pair(p1 x,p2 x)=x.
45 [reference] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1.
46 [reference] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1.
47 [reference] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1.
73 [reference] closedunder pair(closure pair(xs,xf),xf)=p1.
77 [assumption to refute] closedunder pair(closure bad,p2 bad)!=p1.
86 [ur,77,47] closure bad (p2 bad notclosed(closure bad,p2 bad))!=p1.
87 [ur,77,46] closure bad notclosed(closure bad,p2 bad)=p1.
100 [para_into,77.1.2,73.1.2,flip.1] closedunder pair(closure pair(x,y),y)!=closedunder pair(closure bad,p2 bad).
250,249 [ur,86,45,87] closedunder pair(closure bad,p2 bad)=p2.
293 [back_demod,100,demod,250] closedunder pair(closure pair(x,y),y)!=p2.
884 [para_into,293.1.1.2.1.2,13.1.1] closedunder pair(closure x,p2 x)!=p2.
885 [binary,884.1,249.1] $F.