Jonas Kastberg
--- a/theories/logrel/kind_tele.v 0 → 100644
+++ b/theories/logrel/kind_tele.v 0 → 100644
+
+(** An eliminator for elements of [ktele_fun].
+    We use a [fix] because, for some reason, that makes stuff print nicer
+    in the proofs in iris:bi/lib/telescopes.v *)
+Definition ktele_fold {Σ X Y} {kt : ktele Σ}
+    (step : ∀ {k}, (lty Σ k → Y) → Y) (base : X → Y) : (kt -k> X) → Y :=
+  (fix rec {kt} : (kt -k> X) → Y :=
+     match kt as kt return (kt -k> X) → Y with
+     | KTeleO => λ x : X, base x
+     | KTeleS b => λ f, step (λ x, rec (f x))
+     end) kt.
+Arguments ktele_fold {_ _ _ !_} _ _ _ /.
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it *)
+(*   takes to get a [T] from a [kt -t> T]. *)
+Inductive ltys {Σ} : ktele Σ → Type :=