(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 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
9. x1 = y
10. x1 = z
  x1
  =
  if if x1=y z ; x1=z y else x1 fi=x z
  i; if x1=y z ; x1=z y else x1 fi=z x
  ix1=y z
  ix1=z y
  else x1 fi


By: Repeat (SplitOnConclITE THEN MoveToConcl -1)


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