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