proposition: Lemma steps_plus {M} k1 k2 {x} : steps M (k1 + k2) x = obind (fun y => steps M k2 y) (steps M k1 x).
proof: Proof. rewrite /steps Nat.add_comm /Nat.iter nat_rect_plus /= -!/(Nat.iter _ _ _). move: (Nat.iter k1 _ (Some x)) => [y|] /=; first done. apply: oiter_None. Qed.
imports: Undecidability(TM.SBTM) PeanoNat Lia List ssreflect ssrbool ssrfun