proposition: Lemma bind_vis_ {E R U V} (e: E V) (ek: V -> itree E U) (k: U -> itree E R) : observing eq (ITree.bind (Vis e ek) k) (Vis e (fun x => ITree.bind (ek x) k)).
proof: Proof. constructor; reflexivity. Qed.
imports: Coq(Morphisms) ITree(Core.ITreeDefinition)