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