Nuprl - Proof: flip bijection 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: flip bijection 1

1. k :

2. i :

k
3. j :

k
4. a1 :

k
5. a2 :

k
6. (i, j)(a1) = (i, j)(a2)

a1 = a2

By:	MoveToConcl -1 THEN Unfold `flip` 0 THEN Reduce 0 THEN Repeat SplitOnConclITE THEN MoveToConcl -1 THEN Repeat SplitOnConclITE THEN MoveToConcl -1 THEN Repeat SplitOnConclITE THEN MoveToConcl -1 THEN Repeat SplitOnConclITE

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html