proposition: Lemma halt_conf_liftL (c : mconfig sig (state SwitchTM) n) : halt_liftL c = false -> halt (cstate c) = false.
proof: Proof. intros H. cbn. unfold Switch_halt. destruct c as [q t]. now destruct q. Qed.
imports: Undecidability(TM.Util.TM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts