Nuprl - Proof: maximal-in-list 1 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: maximal-in-list 1 2 2

1. A : Type
2. f : A

3. A List
4. u : A
5. u1 : A
6. v1 : A List
7. 0<||[u1 / v1]||+1
8. (

[u1 / v1].(

[u1 / v1].f(x)

f(a)))
9. a : A
10. (a

[u1 / v1])
11. (

[u1 / v1].f(x)

f(a))
12.

f(a)

f(u)

(

[u1 / v1].(

[u; u1 / v1].f(x)

f(a)))

By:	Unfold `l_exists` 0 THEN InstConcl [a]

Generated subgoal:

1 (x[u; u1 / v1].f(x)f(a))
1 step

About:

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