[STATEMENT]
lemma bind_fmap: "bind\<cdot>(fmap\<cdot>f\<cdot>xs)\<cdot>k = bind\<cdot>xs\<cdot>(\<Lambda> x. k\<cdot>(f\<cdot>x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>xs \<bind> k = xs \<bind> (\<Lambda> x. k\<cdot>(f\<cdot>x))
[PROOF STEP]
by (simp add: monad_fmap bind_bind)