Thm* i,j:. i > j Prop

Def hd(l) == Case of l; nil "?" ; h.t h

Thm* A:Type, l:A*. ||l||1 hd(l) A

Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

Thm* A:Type, l:A*. ||l||

Thm* ||nil||

Def map(f;as) == Case of as; nil nil ; a.as' f(a).map(f;as') (recursive)

Thm* A,B:Type, f:(AB), l:A*. map(f;l) B*