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