(3steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: flip twice 1

1. k : 
2. x : k
3. y : k
4. i : k
  ((yx)((yx)(i))) ~ (((yx) o (yx))(i))


By: Reduce 0


Generated subgoals:

None

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

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