proposition: Lemma almost_eq_tape_truncate_tape t : almost_eq_tape (truncate_tape t) t.
proof: Proof. move: t => [[ls a] rs]. constructor; by apply: almost_eq_truncate. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun