proposition: Lemma zip_with_app l1 l2 k1 k2 : length l1 = length k1 → zip_with f (l1 ++ l2) (k1 ++ k2) = zip_with f l1 k1 ++ zip_with f l2 k2.
proof: Proof. rewrite <-Forall2_same_length. induction 1; f_equal/=; auto. Qed.
imports: stdpp(options)