∀(list : Type) → ∀(cons : Natural → list → list) → ∀(nil : list) → list