diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index 452b897780b2b1ae34491b5dbe3bac642c7bdb61..85f075ff9b7468e48e5043f5f8d3838404905833 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -83,8 +83,8 @@ Section proofs.
       iIntros "!==>[HP $]".
       iInv tlN as "[[_ >Hdis2]|>Hitok]" "Hclose".
       + iCombine "Hdis" "Hdis2" as "Hdis".
-        iDestruct (own_valid with "Hdis") as %[_ Hval].
-        revert Hval. rewrite gset_disj_valid_op. set_solver.
+        iDestruct (own_valid with "Hdis") as %[_ Hval%gset_disj_valid_op].
+        set_solver.
       + iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
     - iDestruct (tl_own_disjoint tid {[i]} {[i]} with "[-]") as %?; first by iFrame.
       set_solver.