The ` hd` and ` tl` built-in functions of Lambda--prl
do not exist in
Nuprl
.
They can be simulated with the following definitions.

hd(<a:list>)==list_ind(<a>; "?"; h,t,v.h) tl(<a:list>)==list_ind(<a>; nil; u,v,w.v)Given these definitions, it is straightforward to prove in Nuprl that

>> All A:U1. All L:A list. hd(L) in A => ~(L=nil in A list)and

>> All A:U1. All x:A. All L:A list. hd(x.L)=x in A

Once the two goals above are proved they can be used in other proofs as
lemmas.
Similar facts for ` tl` are also easy to prove.

Thu Sep 14 08:45:18 EDT 1995