fact: Fixpoint mm_list_erase ll i := match ll with | nil => nil | dst::ll => mm_erase dst zero i ++ mm_list_erase ll (2+i) end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MMenv(env mme_defs)