proposition: Lemma ZOOOPST_app : forall A B C xs ys, @zero_or_one_outputs_per_step_trace A B C xs -> zero_or_one_outputs_per_step_trace ys -> zero_or_one_outputs_per_step_trace (xs ++ ys).
proof: Proof. Proof using. induction xs; intros. - auto. - eauto using ZOOOPST_cons_intro, ZOOOPST_head, ZOOOPST_tail. Qed.
imports: Verdi(Verdi HandlerMonad)