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