(17steps 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 lemma 1 2 2

1. k : 
2. x : k
3. y : k
4. z : k
5. y = z
6. x = y
7. x1 : k
8. x1 = x
  y = if y=x z ; y=z x else y fi


By: Repeat SplitOnConclITE


Generated subgoals:

None

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

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