proposition: Lemma NOABT_cons : forall A x y, no_output_at_backup x -> @no_output_at_backup_trace A y -> no_output_at_backup_trace (x :: y).
proof: Proof. Proof using. unfold no_output_at_backup_trace, no_output_at_backup. simpl. intros. intuition; subst; eauto. Qed.
imports: Verdi(Verdi HandlerMonad)