proposition: Lemma ZOOOPST_singleton_singleton : forall A B C h x, @zero_or_one_outputs_per_step_trace A B C [(h, inr [x])].
proof: Proof. Proof using. unfold zero_or_one_outputs_per_step_trace, zero_or_one_outputs_per_step. simpl. intuition. subst. simpl in *. find_inversion. eauto. Qed.
imports: Verdi(Verdi HandlerMonad)