proposition: Theorem interp_interp {E F G R} (f : E ~> itree F) (g : F ~> itree G) : forall t : itree E R, interp g (interp f t) ≅ interp (fun _ e => interp g (f _ e)) t.
proof: Proof. ginit. pcofix CIH. intros. rewrite 2 (unfold_interp t). destruct (observe t); cbn. - rewrite interp_ret. gstep. constructor. reflexivity. - rewrite interp_tau. gstep. constructor. auto with paco. - rewrite interp_bind. guclo eqit_clo_bind. apply pbc_intro_h with (RU := eq). + 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)