proposition: Lemma nth_map2' (A B C : Type) (f : A -> B -> C) (n : nat) (v1 : Vector.t A n) (v2 : Vector.t B n) (k : Fin.t n) : (VectorDef.map2 f v1 v2)[@k] = f v1[@k] v2[@k].
proof: Proof. erewrite VectorSpec.nth_map2; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM