proposition: Lemma MM_cast_length {n} (P : list (mm_instr (Fin.t n))) {m} (E : n = m) : length (MM_cast P E) = length P.
proof: Proof. destruct E. cbn. reflexivity. 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)