fact: Parameter bind_ret : forall {E R S} (r : R) (k : R -> itree E S), ITree.bind (Ret r) k ≈ k r.
imports: Coq(Setoid Morphisms) ITree(Eq.Shallow) ITree.Core.ITreeDefinition ITree.Basics.Basics ITree.Indexed.Sum ITree.Interp.Interp ITree.Interp.Recursion