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
hd satisfies
>> 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.