proposition: Lemma PREPMORE'_length (n' : nat) (H : n' <= n) : length (PREPMORE' n' H) = n'.
proof: Proof. induction n' in H |- *; cbn. - reflexivity. - simpl_list. rewrite IHn'. cbn. lia. 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)