Nuprl - Proof: hevery el

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hevery el

'a:S.

all

(

l:hlist('a). all

(

l:hlist('a). (

P:'a

hbool. equal

(

l:hlist('a). (

P:'a

hbool. (every(P,l)

(

l:hlist('a). (

P:'a

hbool. ,all

(

l:hlist('a). (

P:'a

hbool. ,(

n:hnum. implies

(

l:hlist('a). (

P:'a

hbool. ,(

n:hnum. (lt(n,length(l))

(

l:hlist('a). (

P:'a

hbool. ,(

n:hnum. ,P(el(n,l)))))))

By:	HOL "hevery_el"

Generated subgoals:

None

About:

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