IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip lemma122 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=xz ; y=zx else y fi
By:
Repeat SplitOnConclITE
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html