proposition: Lemma impure_bind_assoc {i α β δ} (p : impure i α) (f : α -> impure i β) (g : β -> impure i δ) : (impure_bind (impure_bind p f) g === impure_bind p (fun x => impure_bind (f x) g))%impure.
proof: Proof. induction p; [reflexivity |]. cbn. change_request_then; auto. reflexivity. Qed.