IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-all-single-decl11212 1. A : Type
2. EqDecider(A)
3. B : AType
4. x:AB(x)Prop
5. x : A 6. B(x)
7. y : A 8. x = y (B(x)) r (B(y))
By:
RevHypSubst -1 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
(B(x)) 
r (B(y))
