Nuprl - Proof: hmap wd

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

'a,'b:S.

and

(all(

f:'a

'b. equal(map(f,nil),nil))

,all

f:'a

'b. all

f:'a

'b. (

h:'a. all

f:'a

'b. (

h:'a. (

t:hlist('a). equal

f:'a

'b. (

h:'a. (

t:hlist('a). (map(f,cons(h,t))

f:'a

'b. (

h:'a. (

t:hlist('a). ,cons(f(h),map(f,t)))))))

By:	HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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