(24steps 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: flip adjacent 1 1 1 1
1. k : 
2. k
3. k
4. x1 : k
5. y1 : k
6. y1-x1 = 0
  (x1, y1) = (x.x)
By: Subst' (y1 = x1) 0

Generated subgoal:

1   (x1, x1) = (x.x)
1 step

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

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