proposition: Lemma simulation_halt q t : TM.halt M q = true -> step (encode_state q, t) = None.
proof: Proof. move: t => [[? ?] ?] /= Hq. by rewrite /= /step /= construct_trans_spec decode_encode_space ?Hq. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun