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 -> 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.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)