[STATEMENT]
lemma actions_min_mdpc_Inr: "actions min_mdpc (Inr b) = {return_pmf (Inr b)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. actions local.min_mdpc (Inr b) = {return_pmf (Inr b)}
[PROOF STEP]
by (simp add: min_mdpc_def map_min_state_R)