proposition: Theorem imonad_law_4_x : forall M (m_dict : IMonad M) I J O A B (f : A -> B) (x : M I J (M J O A)), ijoin (imap (imap f) x) = imap f (ijoin x).
proof: Proof. intros. assert (ijoin (imap (imap f) x) = (ijoin \o imap (imap f)) x). unfold comp. reflexivity. assert (imap f (ijoin x) = (imap f \o ijoin) x). unfold comp. reflexivity. rewrite H. rewrite H0. rewrite imonad_law_4. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality