proposition: Fact mm_set_length n i : length (mm_set n i) = 2+n.
proof: Proof. unfold mm_set; rew length; rewrite mm_incs_length; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)