proposition: Lemma translate_ret : forall (r:R), translate h (Ret r) ≅ Ret r.
proof: Proof. intros r. 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)