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