Nuprl - Proof: hlist not eq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hlist not eq

'a:S.

all

(

l1:hlist('a). all

(

l1:hlist('a). (

l2:hlist('a). implies

(

l1:hlist('a). (

l2:hlist('a). (not(equal(l1,l2))

(

l1:hlist('a). (

l2:hlist('a). ,all

(

l1:hlist('a). (

l2:hlist('a). ,(

h1:'a. all

(

l1:hlist('a). (

l2:hlist('a). ,(

h1:'a. (

h2:'a. not

(

l1:hlist('a). (

l2:hlist('a). ,(

h1:'a. (

h2:'a. (equal

(

l1:hlist('a). (

l2:hlist('a). ,(

h1:'a. (

h2:'a. ((cons(h1,l1)

(

l1:hlist('a). (

l2:hlist('a). ,(

h1:'a. (

h2:'a. (,cons(h2,l2))))))))

By:	HOL "hlist_not_eq"

Generated subgoals:

None

About:

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