proposition: Lemma translate_cmpE : forall E F G R (g : F ~> G) (f : E ~> F) (t : itree E R), translate (f >>> g)%cat t ≅ translate g (translate f t).
proof: Proof. intros E F G R g f t. revert t. ginit. pcofix CIH. intros t. rewrite !unfold_translate. genobs_clear t ot. destruct ot; cbn. - apply reflexivity. - gstep. econstructor. gbase. apply CIH. - gstep. econstructor. intros. gbase. apply CIH. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Core.Subevent Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp)