proposition: Lemma inputs_m_app_inr_singleton : forall tr h l, inputs_m (tr ++ [(h, inr l)]) = inputs_m tr.
proof: Proof. Proof using. intros. rewrite inputs_m_app in *. rewrite inputs_m_inr_singleton in *. rewrite app_nil_r in *. auto. Qed.
imports: Verdi(Verdi HandlerMonad)