proposition: Lemma Forall_zip_with_snd (P : B → Prop) (Q : C → Prop) l k : Forall (λ x, ∀ y, P y → Q (f x y)) l → Forall P k → Forall Q (zip_with f l k).
proof: Proof. intros Hl. revert k. induction Hl; destruct 1; simpl in *; auto. Qed.
imports: stdpp(options)