proposition: Lemma steps_None_mono {M x} k2 k1 : steps M k1 x = None -> k1 <= k2 -> steps M k2 x = None.
proof: Proof. elim: k2 k1 x. { move=> [|k1]; [done|lia]. } move=> k2 IH [|k1] x + ?; first done. rewrite (steps_plus 1 k1) (steps_plus 1 k2). move: (steps M 1 x) => [y|]; last done. move=> /IH. apply. lia. Qed.
imports: Undecidability(TM.SBTM) PeanoNat Lia List ssreflect ssrbool ssrfun