proposition: Lemma outputs_m_app : forall tr1 tr2, outputs_m (tr1 ++ tr2) = outputs_m tr1 ++ outputs_m tr2.
proof: Proof. Proof using. intros. induction tr1; simpl. - auto. - repeat break_match; subst; auto. rewrite <- app_assoc. auto using f_equal. Qed.
imports: Verdi(Verdi HandlerMonad)