Nuprl - Proof: hlength cons 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hlength cons 2

'a:S.

all

(

l:hlist('a). all

(

l:hlist('a). (

n:hnum. equal

(

l:hlist('a). (

n:hnum. (equal(length(l),suc(n))

(

l:hlist('a). (

n:hnum. ,exists

(

l:hlist('a). (

n:hnum. ,(

h:'a. exists

(

l:hlist('a). (

n:hnum. ,(

h:'a. (

l':hlist('a). and

(

l:hlist('a). (

n:hnum. ,(

h:'a. (

l':hlist('a). (equal(length(l'),n)

(

l:hlist('a). (

n:hnum. ,(

h:'a. (

l':hlist('a). ,equal(l,cons(h,l'))))))))

By:	HOL "hlength_cons_2"

Generated subgoals:

None

About:

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