proposition: Lemma Forall_zip_with_ext_l (g : A → B → C) l k1 k2 : Forall (λ x, ∀ y, f x y = g x y) l → k1 = k2 → zip_with f l k1 = zip_with g l k2.
proof: Proof. intros Hl <-. revert k1. by induction Hl; intros [|??]; f_equal/=. Qed.
imports: stdpp(options)