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

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


By: SplitOnConclITE THEN RepeatFor 2 (MoveToConcl -1 THEN 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