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