proposition: Lemma mapM_None_1 l : mapM f l = None → Exists (λ x, f x = None) l.
proof: Proof. induction l as [|x l IH]; simpl; [done|]. destruct (f x) eqn:?; simpl; eauto. by destruct (mapM f l); eauto. Qed.
imports: stdpp(options)