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