[STATEMENT]
lemma map_bind_pmf: "map_pmf f (bind_pmf M g) = bind_pmf M (\<lambda>x. map_pmf f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf f (M \<bind> g) = M \<bind> (\<lambda>x. map_pmf f (g x))
[PROOF STEP]
by (simp add: map_pmf_def bind_assoc_pmf)