proposition: Lemma bind_vis : forall {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. intros; rewrite ITree.Eq.Shallow.bind_vis_; reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree(Eq.Shallow) ITree.Core.ITreeDefinition ITree.Basics.Basics ITree.Indexed.Sum ITree.Interp.Interp ITree.Interp.Recursion ITree(Eq.Eqit Eq.UpToTaus Interp.InterpFacts Interp.RecursionFacts)