proposition: Lemma translate_id : forall E R (t : itree E R), translate (id_ _) t ≅ t.
proof: Proof. intros E R t. revert t. ginit. pcofix CIH. intros t. rewrite itree_eta. rewrite (itree_eta t). rewrite unfold_translate. unfold translateF. destruct (observe t); 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)