IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc reinject12 1. A : Type
2. B : Type
3. y : B inr(y) = InjCase(inr(y); u. inl(u); v. inr(v)) A+B
By:
Reduce Concl
Generated subgoal:
1
inr(y) = inr(y) A+B
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
inr(y) = InjCase(inr(y); u. inl(u); v. inr(v)) 
A+B
