# 24 "natlist.tex" type 'a list = | Nil | Cons of 'a * 'a list # 29 "natlist.tex" type ornament 'a natlist : nat => 'a list with | Z => Nil | S n => Cons (_,n) when n : 'a natlist # 35 "natlist.tex" let _append = lifting add : _ natlist -> _ natlist -> _ natlist # 45 "natlist.tex" let append = lifting add : _ natlist -> _ natlist -> _ natlist with #2 <- match m with Cons (a, _) -> a # 65 "natlist.tex" let map_list = lifting map_nat : ('a -> 'b) -> 'a natlist -> 'b natlist with #2 <- match n with Cons (x, n') -> f x # 81 "natlist.tex" let fold_list = lifting fold_nat : _ -> _ -> 'a natlist -> 'b