diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index acf6978141998ee6aa857cdb15aca7bdc40d3f0a..8c98ea0db570e9a95c261cb9eb2a58968b1db913 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -60,7 +60,7 @@ Section properties.
   Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed.
   Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool.
   Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed.
-  Lemma ltyped_nat Γ (n : Z) : ⊢ Γ ⊨ #n : lty_int.
+  Lemma ltyped_int Γ (i : Z) : ⊢ Γ ⊨ #i : lty_int.
   Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed.
 
   (** Arrow properties *)