Prove lift_bind for the option transformer (MonadTrans.v)

[rudynicolop]

In OptionMonadTransSpec, the proof of lift_bind:

  Lemma lift_bind : forall {M : Type -> Type} `{Monad M}
                      {A B : Type} (m : M A) (f : A -> M B),
      lift (m >>= f) =
      @bind (M ∘ option) (TMonad M) _ _ (lift m) (lift ∘ f).

becomes intractable after a few steps. The Goal seems to be true, but maybe more monad properties are needed in the type class in order to prove it.