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