proposition: Fact mma_instr_compile_length_geq ii : 1 <= mma_instr_compile_length ii.
proof: Proof. cbv; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)