IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-single-pre1-feasible1 1. Id
2. T : Type
3. A : Type
4. x : Id
5. P : ATProp
6. T 7. A 8. a:A. Dec(v:T. P(a,v))
9. x : Ax:Id fp-> Type
xdom(x : A). A=x : A(x) A
By:
Unfold `fpf-all` 0 THEN Unfolds [`fpf-ap`;`fpf-single`] 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
a:A. Dec(
v:T. P(a,v))
x:Id fp-> Type
A
