fact: Definition StateWhile_part : StateWhile_states -> F2 := fun q => match projT2 (pM (projT1 q)) (projT2 q) with | inl _ => default | inr l2 => l2 end.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts