proposition: Lemma steps_plus' {k x k'} : steps (k + k') x = obind (steps k') (steps k x).
proof: Proof. elim: k x. { done. } move=> k IH x /=. case: (mm2_sig_step_dec M x) => [[y]|]; last done. move=> _. by apply: IH. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun