fact: Fixpoint mma_incs k := match k with | 0 => nil | S k => INCₐ x :: mma_incs k end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)