proposition: Lemma almost_eq_tape_steps_None {M k q t1 t2} : almost_eq_tape t1 t2 -> (steps M k (q, t1) = None <-> steps M k (q, t2) = None).
proof: Proof. elim: k q t1 t2; first done. move=> k IH q t1 t2. rewrite !(steps_plus 1 k) /=. case E1: (step M (q, t1)) => [[q2 t'1]|]; case E2: (step M (q, t2)) => [[q'2 t'2]|]. - move: E1 E2 => /almost_eq_tape_step_Some /[apply] /[apply]. move=> [<- /IH]. by apply. - move=> /almost_eq_tape_sym Ht2t1. by move: E2 Ht2t1 E1 => /almost_eq_tape_step_None /[apply] ->. - move=> Ht1t2. by move: E1 Ht1t2 E2 => /almost_eq_tape_step_None /[apply] ->. - done. Qed.
imports: Undecidability(TM.SBTM) PeanoNat Lia List ssreflect ssrbool ssrfun