Nuprl - Proof: hnot eq list

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

'a:S.

all

(

h1:'a. all

(

h1:'a. (

h2:'a. implies

(

h1:'a. (

h2:'a. (not(equal(h1,h2))

(

h1:'a. (

h2:'a. ,all

(

h1:'a. (

h2:'a. ,(

l1:hlist('a). all

(

h1:'a. (

h2:'a. ,(

l1:hlist('a). (

l2:hlist('a). not

(

h1:'a. (

h2:'a. ,(

l1:hlist('a). (

l2:hlist('a). (equal

(

h1:'a. (

h2:'a. ,(

l1:hlist('a). (

l2:hlist('a). ((cons(h1,l1)

(

h1:'a. (

h2:'a. ,(

l1:hlist('a). (

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

By:	HOL "hnot_eq_list"

Generated subgoals:

None

About:

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