IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip lemma2222 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=yz ; x1=zy else x1 fi=xz i; if x1=yz ; x1=zy else x1 fi=zx i; x1=yz i; x1=zy else x1 fi
By:
Repeat (SplitOnConclITE THEN MoveToConcl -1)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html