proposition: Lemma interp_forever {E F} (f : E ~> itree F) {R S} (t : itree E R) : interp f (ITree.forever t) ≅ @ITree.forever F R S (interp f t).
proof: Proof. ginit. pcofix CIH. rewrite (unfold_forever t). rewrite (unfold_forever (interp _ _)). rewrite interp_bind. guclo eqit_clo_bind. econstructor; [reflexivity |]. intros ? _ []. rewrite interp_tau. gstep. constructor; auto with paco. 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)