Nuprl - Proof: fpf-val wf

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

A:Type, B:(A

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

P:(a:{a:A| a

dom(f) }

B(a)

Prop). z != f(x) ==> P(x,z)

Prop

By:	Unfold `fpf-val` 0 THEN FpfSubtype

Generated subgoals:

None

About:

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