Nuprl - Proof: replace fn values wf 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: replace fn values wf 1

1. A : Type
2. X : Type
3. P : A

4. y : A
5. f : X

(

i.if P(f(i))

y else f(i) fi)

By:

Analyze

Generated subgoal:

1 6. i : X
if P(f(i)) y else f(i) fi A
3 steps

About:

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