∀(a : Type)
→ (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)
→ List a