proposition: Lemma ZOOOPST_cons_intro : forall A B C x y, @zero_or_one_outputs_per_step A B C x -> zero_or_one_outputs_per_step_trace y -> zero_or_one_outputs_per_step_trace (x :: y).
proof: Proof. Proof using. unfold zero_or_one_outputs_per_step_trace, zero_or_one_outputs_per_step. simpl. intuition; subst; simpl in *; try discriminate; eauto. Qed.
imports: Verdi(Verdi HandlerMonad)