proposition: Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) (P: B → C → Prop) l1 l2 k : l1 ∈ mapM f k → Forall2 (λ x y, ∀ z, z ∈ f x → P z y) k l2 → Forall2 P l1 l2.
proof: Proof. rewrite elem_of_mapM. intros Hl1. revert l2. induction Hl1; inv 1; constructor; auto. Qed.
imports: stdpp(finite) stdpp(options)