proposition: Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k : l ∈ mapM f k → Forall (λ x, ∀ y, y ∈ f x → P y) k → Forall P l.
proof: Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
imports: stdpp(finite) stdpp(options)