diff --git a/_CoqProject b/_CoqProject
index cbdb539dea7f671e5b7b3235081a59bc146c4704..6b5dd962ad9b155db081ec0173863470237d37cc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -19,7 +19,7 @@ theories/examples/map.v
 theories/examples/map_reduce.v
 theories/examples/subprotocols.v
 theories/logrel/model.v
-theories/logrel/kind_tele.v
+theories/logrel/telescopes.v
 theories/logrel/subtyping.v
 theories/logrel/environments.v
 theories/logrel/term_types.v
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index e772044681557349751c5ba6fa69390c6a1acd62..d7d5f5013272ea153c4363df1f26166fff112917 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -3,7 +3,7 @@ protocols. It includes session types for sending and receiving with session
 polymorphism, as well as n-ary choice. Recursive protocols are defined in
 the model.v file. *)
 From iris.algebra Require Export gmap.
-From actris.logrel Require Export model kind_tele.
+From actris.logrel Require Export model telescopes.
 From actris.channel Require Export channel.
 
 Definition lmsg Σ := iMsg Σ.
diff --git a/theories/logrel/kind_tele.v b/theories/logrel/telescopes.v
similarity index 100%
rename from theories/logrel/kind_tele.v
rename to theories/logrel/telescopes.v
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index b29cec1d0cbc70f104b5cdb2150adbf4e22472b8..aa3ad2ac018d971d599133c52ca7a1513e1fd689 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -35,7 +35,7 @@ use these type formers to define recursive types. *)
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Export spin_lock.
-From actris.logrel Require Export model kind_tele.
+From actris.logrel Require Export model.
 From actris.channel Require Export channel.
 
 Definition lty_unit {Σ} : ltty Σ := Ltty (λ w, ⌜ w = #() ⌝%I).