proposition: Lemma vec_list_vec_change {X n} (v : Vector.t X n) (x : X) (p : pos n) : vec_list (vec_change v p x) = update (proj1_sig (Fin.to_nat p)) (vec_list v) x.
proof: Proof. induction v; cbn. - inversion p. - eapply (Fin.caseS' p); cbn. + cbn. reflexivity. + intros. specialize (IHv p0). destruct (Fin.to_nat p0) eqn:E. cbn in *. now f_equal. 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)