proposition: Lemma outputs_m_inr_primary_singleton : forall h i l, h = Primary -> outputs_m [(h, inr [RequestResponse i l])] = [l].
proof: Proof. Proof using. unfold outputs_m. intros. break_match; auto; congruence. Qed.
imports: Verdi(Verdi HandlerMonad)