proposition: Lemma bind_ret_l {E R S} (r : R) (k : R -> itree E S) : ITree.bind (Ret r) k ≅ (k r).
proof: Proof. apply observing_sub_eqit, bind_ret_. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)