λ(list : Type)
→ λ(cons : Natural → list → list)
→ λ(nil : list)
→ cons +2 (cons +3 (cons +5 nil))