proposition: Lemma almost_eq_tape_step_None M q t1 t2 : almost_eq_tape t1 t2 -> step M (q, t1) = None -> step M (q, t2) = None.
proof: Proof. case=> a ???? [] => [????|n1 n2] [] >. all: rewrite /step /=. all: case: (trans' M _); last done. all: by move=> [[? ?] ?]. Qed.
imports: Undecidability(TM.SBTM) PeanoNat Lia List ssreflect ssrbool ssrfun