Nuprl - Proof: find property 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: find property 1

1. T : Type
2. P : T

3. T List
4. u : T
5. v : T List
6.

d:T.
6. ((first a

v s.t. P(a) else d)

(first a

v s.t. P(a) else d) = d
7. P(u)

d:T. (u

[u / v])

u = d

By:	Auto THEN OrLeft THEN Easy

Generated subgoals:

None

About:

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