Nuprl - Proof: hmap append 2

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

'a,'b:S.

all

(

f:'a

'b. all

(

f:'a

'b. (

l1:hlist('a). all

(

f:'a

'b. (

l1:hlist('a). (

l2:hlist('a). equal

(

f:'a

'b. (

l1:hlist('a). (

l2:hlist('a). (map(f,append(l1,l2))

(

f:'a

'b. (

l1:hlist('a). (

l2:hlist('a). ,append

(

f:'a

'b. (

l1:hlist('a). (

l2:hlist('a). ,(map(f,l1)

(

f:'a

'b. (

l1:hlist('a). (

l2:hlist('a). ,,map(f,l2))))))

By:	HOL "hmap_append_2"

Generated subgoals:

None

About:

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