proposition: Lemma NOABT_app : forall A xs ys, @no_output_at_backup_trace A xs -> no_output_at_backup_trace ys -> no_output_at_backup_trace (xs ++ ys).
proof: Proof. Proof using. induction xs; intros; simpl in *; auto. eauto using NOABT_cons, NOABT_head, NOABT_tail. Qed.
imports: Verdi(Verdi HandlerMonad)