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