proposition: Lemma bind_trigger {E R} U (e : E U) (k : U -> itree E R) : ITree.bind (ITree.trigger e) k ≅ Vis e (fun x => k x).
proof: Proof. rewrite unfold_bind; cbn. pstep. constructor. intros; red. left. apply bind_ret_l. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)