IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-single wf1 1. A : Type
2. B : AType
3. x : A 4. v : B(x)
5. x1 : A 6. x1 = x vB(x1)
By:
Assert (B(x1) = B(x)) THEN Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
v 
B(x1)
