proposition: Lemma steps_truncate {M k q t} : steps M k (q, truncate_tape t) = None <-> (steps M k (q, t) = None).
proof: Proof. apply: almost_eq_tape_steps_None. apply: almost_eq_tape_truncate_tape. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun