proposition: Lemma interp_translate {E F G} (f : E ~> F) (g : F ~> itree G) {R} (t : itree E R) : interp g (translate f t) ≅ interp (fun _ e => g _ (f _ e)) t.
proof: Proof. revert t. ginit. pcofix CIH. intros t. rewrite !unfold_interp. unfold _interp. rewrite unfold_translate_. unfold translateF. destruct (observe t); cbn. - apply reflexivity. - gstep. constructor. gbase. apply CIH. - guclo eqit_clo_bind; econstructor. + reflexivity. + intros ? _ []. 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)