IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
same range sep wf inj1 1. A : Type
2. B : Type
same_range_sep(A; B) (A injB)(A injB)Prop
By:
(A injB) (AB) By Def of A injB
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
same_range_sep(A; B) 
(A inj
B)
(A inj
(A
