proposition: Lemma NOABT_tail : forall A x y, @no_output_at_backup_trace A (x :: y) -> no_output_at_backup_trace y.
proof: Proof. Proof using. unfold no_output_at_backup_trace. intros. simpl in *. eauto. Qed.
imports: Verdi(Verdi HandlerMonad)