diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 9445b8c7acc8822c09433bd4320184e0b8703942..9e09a8c806eca2325f81b5a41ba8333d1327a10c 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -28,7 +28,7 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I.
 Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I.
-Definition lty_texist {Σ} {TT : ktele Σ} (C : kt → ltty Σ) : ltty Σ :=
+Definition lty_texist {Σ} {kt : ktele Σ} (C : ltys kt → ltty Σ) : ltty Σ :=
   ktele_fold (@lty_exist Σ) (λ x, x) (ktele_bind C).
 
 Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,