Nuprl - Proof: hel wd

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

'a:S.

and

(all(

l:hlist('a). equal(el(0,l),hd(l)))

,all(

l:hlist('a). all(

n:hnum. equal(el(suc(n),l),el(n,tl(l))))))

By:	WOSimp (ioid !oid{hel simp update:s}) (WOSimp (ioid !oid{hdd simp update:s}) HN)

Generated subgoals:

1 1. 'a : S
2. l : hlist('a)
el(0,l) = hd(l)
1 step

2 1. 'a : S
2. l : hlist('a)
3. n :
el(n+1,l) = el(n,tl(l))
4 steps

About:

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

1	1. 'a : S 2. l : hlist('a) el(0,l) = hd(l)	1 step
2	1. 'a : S 2. l : hlist('a) 3. n : el(n+1,l) = el(n,tl(l))	4 steps