proposition: Lemma StateWhileInduction : (forall tin l yout tout (HLastStep: R1 l tin (inr yout, tout)), R2 l tin (yout, tout)) -> (forall tin l l' tmid tout yout (HStar : R1 l tin (inl l', tmid)) (HLastStep : R2 l' tmid (yout, tout)), R2 l tin (yout, tout)) -> (forall l, StateWhile_Rel R1 l <<=2 (R2 l)).
proof: Proof. intros H1 H2. intros tin tout. induction 1; eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.DepPairs EqdepFacts