diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 27a30a516a49ecc868b8a1ce4252c944a0578b7e..85a975a569330dd57bfd1388297b2b532984f02a 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -186,10 +186,10 @@ Section rdcss.
   (* After the prophecy said we are going to win the race, we commit and run the AU,
      switching from [pending] to [accepted]. *)
   Definition accepted_state Q (proph_winner : option proph_id) (p_ghost_winner : proph_id) :=
-    ((∃ vs, proph p_ghost_winner vs) ∗
+    ((∃ vs, proph p_ghost_winner vs) ∗ Q ∗
      match proph_winner with
        None => True
-     | Some p => ⌜p = p_ghost_winner⌝ ∗ Q
+     | Some p => ⌜p = p_ghost_winner⌝
      end)%I.
 
   (* The same thread then wins the CmpXchg and moves from [accepted] to [done].
@@ -342,7 +342,7 @@ Section rdcss.
     wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_suc.
     iIntros (vs'' ->) "Hp'". simpl.
     (* Update to Done. *)
-    iDestruct "Accepted" as "[Hp_phost_inv [HEq Q]]".
+    iDestruct "Accepted" as "[Hp_phost_inv [Q Heq]]".
     iMod (own_update with "Hs") as "Hs".
     { apply (cmra_update_exclusive (Cinr (to_agree ()))). done. }
     iDestruct "Hs" as "#Hs'". iModIntro.
@@ -378,7 +378,7 @@ Section rdcss.
         iIntros (vs'' ->). simpl.
         iDestruct "State" as "[Pending | Accepted]".
         + iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
-        + iDestruct "Accepted" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+        + iDestruct "Accepted" as "[_ [_ Hvs]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
     }
     (* So, we know our protocol is [Done]. *)
     (* It must be that (state_to_val s) ≠ (InjRV l_descr) because we are in the failing thread. *)