∀ {m : Type u → Type v} [inst : Monad m],
  (∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β) →
    (∀ {α : Type u} (x : m α), id <$> x = x) →
      (∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x) →
        (∀ {α β : Type u} (x : m α) (y : m β), x <* y = Function.const β <$> x <*> y) →
          (∀ {α β : Type u} (x : m α) (y : m β), x *> y = Function.const α id <$> x <*> y) →
            (∀ {α β : Type u} (g : α → β) (x : m α), pure g <*> x = g <$> x) →
              (∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)) →
                (∀ {α β : Type u} (g : m (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g) →
                  (∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)),
                      h <*> (g <*> x) = Function.comp <$> h <*> g <*> x) →
                    (∀ {α β : Type u} (f : α → β) (x : m α),
                        (do
                            let a ← x
                            pure (f a)) =
                          f <$> x) →
                      (∀ {α β : Type u} (f : m (α → β)) (x : m α),
                          (do
                              let x_1 ← f
                              x_1 <$> x) =
                            f <*> x) →
                        (∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) →
                          (∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ),
                              x >>= f >>= g = x >>= fun x => f x >>= g) →
                            LawfulMonad m