proposition: Lemma mapM_fmap_Forall2_Some_inv (g : B → A) (l : list A) (k : list B) : mapM f l = Some k → Forall2 (λ x y, f x = Some y → g y = x) l k → g <$> k = l.
proof: Proof. induction 2; simplify_option_eq; naive_solver. Qed.
imports: stdpp(options)