proposition: Lemma interp_iter' {E F} (f : E ~> itree F) {I A} (t : I -> itree E (I + A)) (t' : I -> itree F (I + A)) (EQ_t : forall i, eq_itree eq (interp f (t i)) (t' i)) : forall i, interp f (ITree.iter t i) ≅ ITree.iter t' i.
proof: Proof. ginit. pcofix CIH; intros i. rewrite 2 unfold_iter. rewrite interp_bind. guclo eqit_clo_bind; econstructor; eauto. { apply EQ_t. } intros [] _ []; cbn. - rewrite interp_tau; gstep; constructor; auto with paco. - rewrite interp_ret. gstep; constructor; auto. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp Interp.Handler Interp.TranslateFacts)