(31steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: permute by flips 1 1
1. p : 00
2. Bij(0; 0; p)
  p = (x.x)
By: Ext THEN Reduce 0

Generated subgoals:

None

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

(31steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc