(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 2

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


By: RWO Thm* k:x,y:k. (yx) o (yx) = (x.x) 0 THEN Reduce 0


Generated subgoals:

None

About:
intnatural_numberlambdaapplyfunctionequalall
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