diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index 882fb38721c99d44e68884cc9db56f90e5671b81..86db05b0aea3899f51649388fd305ce3feec919e 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -80,7 +80,7 @@ Section proofs.
     iIntros (??) "#Htlinv Htoks".
     iDestruct "Htlinv" as (i) "[% #Hinv]".
     rewrite {1 4}(union_difference_L (nclose N) E) //.
-    rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.    
+    rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_tokens_union; try set_solver.
     iDestruct "Htoks" as "[[Htoki Htoks0] Htoks1]". iFrame "Htoks0 Htoks1".
     iInv tlN as "[[HP >Hdis]|>Htoki2]" "Hclose".
     - iVs ("Hclose" with "[Htoki]") as "_". auto. iFrame.