proposition: Lemma mapM_Some_1 l k : mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
proof: Proof. revert k. induction l as [|x l]; intros [|y k]; simpl; try done. - destruct (f x); simpl; [|discriminate]. by destruct (mapM f l). - destruct (f x) eqn:?; intros; simplify_option_eq; auto. Qed.
imports: stdpp(options)