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

(10steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

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

1. A : Type
2. f : A

3. A List
4. u : A
5. 0<||nil||

(

a

nil.(

x

nil.f(x)

f(a)))
6. 0<||nil||+1

(u

[u])

By:	RWO Thm* a,x:T. (x [a]) x = a 0

Generated subgoals:

None

About:

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

(10steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc