proposition: Lemma trace_outputs_app : forall tr1 tr2, trace_outputs (tr1 ++ tr2) = trace_outputs tr1 + trace_outputs tr2.
proof: Proof. unfold trace_outputs. intros. rewrite filterMap_app. rewrite app_length. auto. Qed.
imports: Verdi(Verdi HandlerMonad)