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