diff --git a/base_logic/lib/na_invariants.v b/base_logic/lib/na_invariants.v
index 2a4fe80136b6befa04aa4f5797e998f918917328..508b88300b038e91ad2219c7ae5b43a557f9acff 100644
--- a/base_logic/lib/na_invariants.v
+++ b/base_logic/lib/na_invariants.v
@@ -71,14 +71,14 @@ Section proofs.
     iNext. iLeft. by iFrame.
   Qed.
 
-  Lemma na_inv_open tid E N P :
-    â†‘N âŠ† E â†’
-    na_inv tid N P -âˆ— na_own tid E ={E}=âˆ— â–· P âˆ— na_own tid (Eâˆ–â†‘N) âˆ—
-                       (â–· P âˆ— na_own tid (Eâˆ–â†‘N) ={E}=âˆ— na_own tid E).
+  Lemma na_inv_open tid E F N P :
+    â†‘N âŠ† E â†’ â†‘N âŠ† F â†’
+    na_inv tid N P -âˆ— na_own tid F ={E}=âˆ— â–· P âˆ— na_own tid (Fâˆ–â†‘N) âˆ—
+                       (â–· P âˆ— na_own tid (Fâˆ–â†‘N) ={E}=âˆ— na_own tid F).
   Proof.
-    rewrite /na_inv. iIntros (?) "#Htlinv Htoks".
+    rewrite /na_inv. iIntros (??) "#Htlinv Htoks".
     iDestruct "Htlinv" as (i) "[% Hinv]".
-    rewrite [E as X in na_own tid X](union_difference_L (â†‘N) E) //.
+    rewrite [F as X in na_own tid X](union_difference_L (â†‘N) F) //.
     rewrite [X in (X âˆª _)](union_difference_L {[i]} (â†‘N)) ?na_own_union; [|set_solver..].
     iDestruct "Htoks" as "[[Htoki $] $]".
     iInv N as "[[$ >Hdis]|>Htoki2]" "Hclose".