proposition: Fact mm_multi_copy_length k src dst i : length (mm_multi_copy k src dst i) = 9*k.
proof: Proof. revert src dst i; induction k as [ | k IHk ]; intros src dst i; simpl; auto. rew length; rewrite IHk; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)