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