proposition: Lemma vec_app_spec {X n m} (v : Vector.t X n) (w : Vector.t X m) : vec_app v w = Vector.append v w.
proof: Proof. induction v. - cbn. eapply vec_pos_ext. intros. now rewrite vec_pos_set. - rewrite vec_app_cons. cbn. congruence. 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)