proposition: Lemma map2_ext A B C: forall (f g:A->B->C), (forall a b, f a b = g a b) -> forall n (v : t A n) (w : t B n), map2 f v w = map2 g v w.
proof: Proof. intros f g Hfg n v w. apply (fun P H1 H2 => rect2 P H1 H2 v w). - reflexivity. - cbn. intros ??? IH ??. now rewrite IH, Hfg. Qed.
imports: VectorDef PeanoNat Eqdep_dec