IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-cap-single12 1. A : Type
2. eq : EqDecider(A)
3. x : A 4. v : Top
5. z : Top
if true false <[x],x.v>(x) else z fi ~ v
By:
Unfold `fpf-ap` 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
if true
<[x],
x.v>(x) else z fi ~ v
