proposition: Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 : Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 → Forall2 P (l1 ≫= f) (l2 ≫= g).
proof: Proof. induction 1; csimpl; auto using Forall2_app. Qed.
imports: stdpp(options)