proposition: Lemma Forall_zip_with_fst (P : A → Prop) (Q : C → Prop) l k : Forall P l → Forall (λ y, ∀ x, P x → Q (f x y)) 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)