Nuprl - Proof: hcons 11

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

'a:S.

all

(

h:'a. all

(

h:'a. (

t:hlist('a). all

(

h:'a. (

t:hlist('a). (

h':'a. all

(

h:'a. (

t:hlist('a). (

h':'a. (

t':hlist('a). equal

(

h:'a. (

t:hlist('a). (

h':'a. (

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

(

h:'a. (

t:hlist('a). (

h':'a. (

t':hlist('a). ,and

(

h:'a. (

t:hlist('a). (

h':'a. (

t':hlist('a). ,(equal(h,h')

(

h:'a. (

t:hlist('a). (

h':'a. (

t':hlist('a). ,,equal(t,t')))))))

By:	HOL "hcons_11"

Generated subgoals:

None

About:

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