proposition: Lemma eutt_interp_state_iter {E F S A A' B B'} (RA : A -> A' -> Prop) (RB : B -> B' -> Prop) (RS : S -> S -> Prop) (h : E ~> Monads.stateT S (itree F)) (t1 : A -> itree E (A + B)) (t2 : A' -> itree E (A' + B')) : (forall ca ca' s1 s2, RS s1 s2 -> RA ca ca' -> eutt (prod_rel RS (sum_rel RA RB)) (interp_state h (t1 ca) s1) (interp_state h (t2 ca') s2)) -> (forall a a' s1 s2, RS s1 s2 -> RA a a' -> eutt (fun a b => RS (fst a) (fst b) /\ RB (snd a) (snd b)) (interp_state h (iter (C := ktree _) t1 a) s1) (interp_state h (iter (C := ktree _) t2 a') s2)).
proof: Proof. apply eutt_interp_state_aloop. Qed.
imports: Coq(Program.Tactics Morphisms) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.HeterogeneousRelations Basics.Monad Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Interp.Interp Interp.InterpFacts Interp.RecursionFacts Events.State)