proposition: Lemma ZOOOPST_tail : forall A B C x y, @zero_or_one_outputs_per_step_trace A B C (x :: y) -> zero_or_one_outputs_per_step_trace y.
proof: Proof. Proof using. unfold zero_or_one_outputs_per_step_trace, zero_or_one_outputs_per_step. simpl. eauto. Qed.
imports: Verdi(Verdi HandlerMonad)