proposition: Lemma startState_irrelevant k l l' c1 c2 : loopM (StateWhileTM l ) c1 k = Some c2 -> loopM (StateWhileTM l') c1 k = Some c2.
proof: Proof. auto. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts