diff --git a/racket/typed/leader-and-seller.pml b/racket/typed/leader-and-seller.pml
index 3bb4b59..e8a8597 100644
--- a/racket/typed/leader-and-seller.pml
+++ b/racket/typed/leader-and-seller.pml
@@ -163,6 +163,10 @@ ltl sanity {
      BoTM_assertions >= 0)
   &&
   <> (BQ_assertions > 0)
+  &&
+  [] (ASSERTED(IBQ) -> <> ASSERTED(BQ))
+  &&
+  [] (ASSERTED(IBI) -> <> ASSERTED(BI))
   /*
   &&
   <> (leader_state == announce || leader_state == none)