proposition: Lemma bind_vis {E R} U V (e: E V) (ek: V -> itree E U) (k: U -> itree E R) : ITree.bind (Vis e ek) k ≅ Vis e (fun x => ITree.bind (ek x) k).
proof: Proof. apply (unfold_bind (Vis e ek) k). Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)