proposition: Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k : Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
proof: Proof. intros Hl. revert k. induction Hl; set_solver. Qed.
imports: stdpp(finite) stdpp(options)