proposition: Lemma lifth_comp l (c : mconfig sig (state (StateWhileTM l)) n) : lifth c = false -> haltConf c = false.
proof: Proof. destruct c as ((l'&q)&t). cbn. decide (l=l') as [->| _]; intros H; [|easy]. unfold StateWhile_halt. cbn. now rewrite H. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts