diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 80202624a5fba1ce3c559cab273d152dc64cb58e..a675d227b639ed8990f93f92b475b34715235fb0 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -113,8 +113,14 @@ Proof.
   rewrite -own_op own_valid auth_both_validI /=. iIntros "[_ [#HI #HvI]]".
   iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
   iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
-  (*rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.*)
-  rewrite lookup_fmap (lookup_op (A:=agreeR (laterO (iPrePropO Σ)))).
+  Fail rewrite lookup_fmap lookup_op lookup_singleton bi.option_equivI.
+  rewrite lookup_fmap.
+  Set Typeclasses Debug. Fail rewrite lookup_op. Unset Typeclasses Debug.
+  (* Failed TC search for `(ElemOf ?T (agreeR (laterO (iPrePropO
+  Σ))))`. The [singletonM] on the LHS of the [̧(⋅)] we want to rewrite
+  has [A := agree (later (ofe_car (iPrePropO Σ)))], not [agreeR ...].
+  *)
+  rewrite (lookup_op (A:=agreeR (laterO (iPrePropO Σ)))).
   rewrite lookup_singleton bi.option_equivI.
   case: (I !! i)=> [Q|] /=; [|case: (I' !! i)=> [Q'|] /=; by iExFalso].
   iExists Q; iSplit; first done.