proposition: Theorem imonad_law_1_x : forall M (m_dict : IMonad M) I J K O A (x : M I J (M J K (M K O A))), ijoin (imap ijoin x) = (@ijoin M m_dict _ _ _ A) (ijoin x).
proof: Proof. intros. assert (ijoin (imap ijoin x) = (ijoin \o imap ijoin) x). unfold comp. reflexivity. assert (ijoin (ijoin x) = (ijoin \o ijoin) x). unfold comp. reflexivity. rewrite H. rewrite H0. rewrite imonad_law_1. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality