proposition: Lemma translate_tau : forall (t : itree E R), translate h (Tau t) ≅ Tau (translate h t).
proof: Proof. intros t. rewrite itree_eta, unfold_translate. cbn. reflexivity. 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)