fact: Fixpoint mm_nullify i lr := match lr with | nil => nil | x::lr => mm_null x zero i ++ mm_nullify (2+i) lr end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)