IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fin plus nat ooc nat122 1. k : 2. y : InjCase(if y<k inl(y) else inr(y-k) fi; i. i; n. k+n) = y
By:
SplitOnConclITE THEN Reduce Concl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
InjCase(if y<
k
inl(y) else inr(y-k) fi; i. i; n. k+n) = y
