proposition: Lemma inputs_m_app : forall l1 l2, inputs_m (l1 ++ l2) = inputs_m l1 ++ inputs_m l2.
proof: Proof. Proof using. unfold inputs_m. intros. induction l1; simpl; repeat break_match; subst; simpl in *; auto using f_equal. Qed.
imports: Verdi(Verdi HandlerMonad)