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

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

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].f(x)

f(u))

By:	RepeatFor 2 (ParallelOp -2) THEN ParallelOp -1

Generated subgoals:

None

About:

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