proposition: Lemma StateWhile_split_break k l l2 c2 c3 : loop (step (StateWhileTM l)) (haltConf (M:=StateWhileTM l)) (lift c2) k = Some c3 -> haltConf c2 = true -> projT2 (pM l) (cstate c2) = inr l2 -> c3 = lift c2.
proof: Proof. intros HLoop H E. eapply loop_eq_0 in HLoop; auto. unfold haltConf in *. cbn in *. unfold StateWhile_halt in *. cbn in *. now rewrite H, E. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts