proposition: Lemma nth_error_vec_list {X n} (v : Vector.t X n) m (H : m < n) x : nth_error (vec_list v) m = Some x -> vec_pos v (Fin.of_nat_lt H) = x.
proof: Proof. induction v in m , H |- *; cbn. - lia. - destruct m; cbn. + congruence. + eapply IHv. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)