proposition: Lemma Vector_map2_ext {A B C} (f g : A -> B -> C) n (v1 : Vector.t A n) (v2 : Vector.t B n) : (forall a b, f a b = g a b) -> Vector.map2 f v1 v2 = Vector.map2 g v1 v2.
proof: Proof. intros H. pattern n, v1, v2; revert n v1 v2. eapply Vector.rect2. - reflexivity. - intros n v1 v2 IH a b. cbn. now rewrite H, IH. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM