fact: Definition lift {l : F1} (c : mconfig sig (state (projT1 (pM l))) n) : mconfig sig (FinType(EqType StateWhile_states)) n := {| cstate := liftState (cstate c); ctapes := ctapes c; |}.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts