proposition: Lemma eutt_iter'' {E I1 I2 R1 R2} (RI1 RI2 : I1 -> I2 -> Prop) (HSUB: RI2 <2= RI1) (RR : R1 -> R2 -> Prop) (body1 : I1 -> itree E (I1 + R1)) (body2 : I2 -> itree E (I2 + R2)) (eutt_body : forall j1 j2, RI1 j1 j2 -> eutt (sum_rel RI2 RR) (body1 j1) (body2 j2)) : forall (i1 : I1) (i2 : I2) (RI_i : RI1 i1 i2), @eutt E _ _ RR (ITree.iter body1 i1) (ITree.iter body2 i2).
proof: Proof. einit. ecofix CIH. intros. specialize (eutt_body i1 i2 RI_i). do 2 rewrite unfold_iter. ebind; econstructor; eauto with paco. intros ? ? []. - etau. - eauto with paco. Qed.
imports: Coq(Classes.Morphisms Setoids.Setoid Relations.Relations) Paco(paco) ITree(Basics.Basics Basics.CategoryOps Basics.CategoryTheory Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Function Basics.HeterogeneousRelations Core.ITreeDefinition Core.ITreeMonad Core.KTree Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2)