proposition: Lemma bind_ret_r {E R} : forall s : itree E R, ITree.bind s (fun x => Ret x) ≅ s.
proof: Proof. ginit. pcofix CIH. intros. rewrite (itree_eta_ (ITree.bind _ _)), (itree_eta s). cbn. destruct (observe s); cbn; gstep; constructor; eauto with paco itree. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)