(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

  k:x,y,i:k. (yx)((yx)(i)) = i

By: Auto THEN Subst (((yx)((yx)(i))) ~ (((yx) o (yx))(i))) 0


Generated subgoals:

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

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

1 step

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