proposition: Fact mm_list_erase_length ll i : length (mm_list_erase ll i) = 2*length ll.
proof: Proof. revert i; induction ll as [ | dst ll IH ]; simpl; intros i; rew length; auto. rewrite IH; ring. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)