proposition: Lemma vec_pos_nth_eq {X : Type} {n} {v : Vector.t X n} {i} : vec_pos v i = Vector.nth v i.
proof: Proof. elim: v i. { by apply: Fin.case0. } move=> > IH i. have [->|[? ->]] := pos_S_inv i. - done. - apply: IH. Qed.
imports: Undecidability.TM(TM) Undecidability.MinskyMachines(MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Undecidability.Shared.Libs.PSL(CompoundFinTypes) Undecidability.Shared.Libs.PSL.EqDec List Lia PeanoNat Compare_dec Relations ssreflect ssrbool ssrfun