proposition: Lemma NOABT_contra : forall A l tr, @no_output_at_backup_trace A ((Backup, inr l) :: tr) -> l = [] \/ exists d, l = [ReadResponse d].
proof: Proof. Proof using. unfold no_output_at_backup_trace, no_output_at_backup. intros. simpl in *. find_insterU. econcludes. find_insterU. simpl in *. econcludes. intuition. repeat break_match; intuition eauto. Qed.
imports: Verdi(Verdi HandlerMonad)