proposition: Theorem imonad_assoc : forall M `{IMonad M} {I J K L A B C} (m : M I J A) (f : A -> M J K B) (g : B -> M K L C), (m >>= f) >>= g = m >>= (fun x => f x >>= g).
proof: Proof. intros. unfold ibind. rewrite <- imonad_law_4_x. rewrite ifun_composition_x. rewrite <- imonad_law_1_x. rewrite ifun_composition_x. f_equal. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality