proposition: Lemma mm2_progress (mmi: mm2_instr) (x: mm2_state) : { y | mm2_atom mmi x y }.
proof: Proof. move: x mmi => [i [[|a] [|b]]] [||j|j]; eexists; by constructor. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun