Proof about monadic functions

Stream: new members

[Jannis Limperg]

I'm struggling a little with a proof that two monadic functions are equal. I'll post the full proof for critique when it's done, but for now I just need this lemma:

import tactic

lemma bind_const {α β m} [monad m] [is_lawful_monad m] (ma : m α) (mb : m β) :
  (ma >>= λ _, mb) = mb := by library_search -- fails :(

[Reid Barton]

Isn't this false though?

[Reid Barton]

for example, [] >>= (\lam _, [1]) = []

[Jannis Limperg]

Meh, you're right. Back to the drawing board.