proposition: Lemma Forall_bind (P : B → Prop) l : Forall P (l ≫= f) ↔ Forall (Forall P ∘ f) l.
proof: Proof. split. - induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition. - induction 1; csimpl; rewrite ?Forall_app; auto. Qed.
imports: stdpp(options)