Nuprl - Proof: hflat wd

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

'a:S.

and

(equal(flat(nil),nil)

,all

h:hlist('a). all

h:hlist('a). (

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

h:hlist('a). (

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

h:hlist('a). (

t:hlist(hlist('a)). ,append(h,flat(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