diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 69cabd270f4e88e5dfe391742f69dc072231e4bf..cba58c5b63671aba8812fcdb1c0d327c91467b78 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -203,8 +203,7 @@ Section mapsto.
   Proof.
     iIntros "Hl1 Hl2".
     iDestruct (mapstoS_agree with "Hl1 Hl2") as %?. simplify_eq.
-    iSplit; eauto.
-    iApply (fractional_half_2 with "Hl1 Hl2").
+    iSplit; eauto. iCombine "Hl1 Hl2" as "?". done.
   Qed.
 
 End mapsto.