[STATEMENT]
lemma map_resource_compose [simp]:
  "map_resource a b (map_resource a' b' res) = map_resource (a' \<circ> a) (b \<circ> b') res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_resource a b (map_resource a' b' res) = map_resource (a' \<circ> a) (b \<circ> b') res
[PROOF STEP]
by(coinduction arbitrary: res)(auto 4 3 intro!: rel_funI rel_spmf_reflI simp add: spmf_rel_map)