proposition: Lemma vec_list_vec_app {X n m} (v : Vector.t X n) (w : Vector.t X m) : vec_list (vec_app v w) = vec_list v ++ vec_list w.
proof: Proof. rewrite ! vec_app_spec. induction v in w |- *. - cbn. reflexivity. - cbn. f_equal. eauto. 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)