IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-compatible-singles2 1. A : Type
2. EqDecider(A)
3. B : AType
4. x : A 5. y : A 6. B(x)
7. u : B(y)
8. x = y uB(x)
By:
DoSubsume THEN HypSubst -1 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
u 
B(x)
