proposition: Lemma bind_ret_r' {E R} (u : itree E R) (f : R -> R) : (forall x, f x = x) -> ITree.bind u (fun r => Ret (f r)) ≅ u.
proof: Proof. intro H. rewrite <- (bind_ret_r u) at 2. apply eqit_bind. - reflexivity. - hnf. intros. apply eqit_Ret. auto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)