@@ -69,7 +69,6 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
6969 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
7070 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
7171
72−-- The believe_me is there because idris won't seem to unify (pure x = Just x) with Refl
7372VerifiedMonad Maybe where
7473 monadApplicative Nothing Nothing = Refl
7574 monadApplicative Nothing (Just x) = Refl
@@ -77,7 +76,7 @@ VerifiedMonad Maybe where
7776 monadApplicative (Just x) (Just y) = Refl
7877 monadLeftIdentity x f = Refl
7978 monadRightIdentity Nothing = Refl
80− monadRightIdentity (Just x) = (believe_me (Refl {A = Maybe a} {x = Just x}))
79+ monadRightIdentity (Just x) = Refl
8180 monadAssociativity Nothing f g = Refl
8281 monadAssociativity (Just x) f g = Refl
8382