proposition: Lemma lifth_comp' l (c : mconfig sig (state (projT1 (pM l))) n) : @lifth l (lift c) = haltConf c.
proof: Proof. unfold haltConf. destruct c as (q,t). cbn. decide (l=l); tauto. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts