IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-all-single-decl113111 1. A : Type
2. EqDecider(A)
3. B : AType
4. P : x:AB(x)Prop
5. x : A 6. v : B(x)
7. P(x,v)
8. y : A 9. x = y 10. z : A 11. z = x (B(x)) r (B(z))
By:
HypSubst -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(z))
