Nuprl - Proof: fpf-ap wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-ap wf

A:Type, B:(A

Type), f:a:A fp-> B(a), eq:EqDecider(A), x:A.

dom(f)

f(x)

B(x)

By:	Unfolds [`fpf`;`fpf-dom`;`fpf-ap`] 0

Generated subgoal:

1 1. A : Type
2. B : AType
3. f : d:A Lista:{a:A| (a d) }B(a)
4. eq : EqDecider(A)
5. x : A
6. deq-member(eq;x;1of(f))
x {a:A| (a 1of(f)) }
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html