(4steps total) PrintForm Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: flip bijection 2 1
1. k : 
2. i : k
3. j : k
4. b : k
  (i, j)((i, j)(b)) = b
By: Unfold `flip` 0 THEN Reduce 0 THEN Repeat (SplitOnConclITE THEN MoveToConcl -1)

Generated subgoals:

None

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

(4steps total) PrintForm Definitions mb nat Sections MarkB generic Doc