∀(a : Type) → List a → List a