proposition: Lemma inputs_m_on_cons : forall t tr, inputs_m (t :: tr) = match t with | (Primary, inl (Request i)) => i :: inputs_m tr | _ => inputs_m tr end.
proof: Proof. Proof using. unfold inputs_m. intros. simpl. repeat break_match; repeat find_inversion; auto; try discriminate. Qed.
imports: Verdi(Verdi HandlerMonad)