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