fact: Fixpoint mma_null_list (l : list (pos n)) i := match l with | nil => nil | x::l => DECₐ x i :: mma_null_list l (S i) end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)