diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 0ef44e018b82cf1bfba17a04ff8d95d10d7e032a..f583c71d40b16e0a1bae56f890cbe70d91f5e80b 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -503,12 +503,12 @@ Section fundamental.
     - by iApply (bin_log_related_CmpXchg with "[] []").
   Qed.
 
-  Theorem refines_typed e Ï„ :
+  Theorem refines_typed τ Δ e :
     ∅ ⊢ₜ e : τ →
-    REL e << e : (interp Ï„ []).
+    REL e << e : (interp τ Δ ).
   Proof.
     move=> /binary_fundamental Hty.
-    iPoseProof (Hty [] with "[]") as "H".
+    iPoseProof (Hty Δ with "[]") as "H".
     { rewrite fmap_empty. iApply env_ltyped2_empty. }
     by rewrite !fmap_empty !subst_map_empty.
   Qed.