proposition: Lemma elem_of_mapM {A B} (f : A → M B) l k : l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
proof: Proof. split. - revert l. induction k; set_solver by eauto. - induction 1; set_solver. Qed.
imports: stdpp(finite) stdpp(options)