proposition: Lemma halt_comp (l : F1) (c : mconfig sig (state (projT1 (pM l))) n) : haltConf (M := projT1 (pM l)) c = false -> haltConf (M := StateWhileTM l) (lift c) = false.
proof: Proof. intros HHalt. cbn in *. destruct c as [q t]. cbn in *. apply andb_false_iff. cbn. now left. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts