From d070e44a40282a8564be5b76b4c8f88bebdaa495 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jun 2018 09:40:43 +0200
Subject: [PATCH] rename lemmas about telescope function space to tele_fun_*

---
 theories/telescopes.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/telescopes.v b/theories/telescopes.v
index 40011932..8e68e3cc 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -106,19 +106,19 @@ Qed.
 
 (** We can define the identity function and composition of the [-t>] function
 space. *)
-Definition tele_id {TT : tele} : TT -t> TT := tele_bind id.
+Definition tele_fun_id {TT : tele} : TT -t> TT := tele_bind id.
 
-Lemma tele_id_eq {TT : tele} (x : TT) :
-  tele_id x = x.
-Proof. unfold tele_id. rewrite tele_app_bind. done. Qed.
+Lemma tele_fun_id_eq {TT : tele} (x : TT) :
+  tele_fun_id x = x.
+Proof. unfold tele_fun_id. rewrite tele_app_bind. done. Qed.
 
-Definition tele_compose {TT1 TT2 TT3 : tele} :
+Definition tele_fun_compose {TT1 TT2 TT3 : tele} :
   (TT2 -t> TT3) → (TT1 -t> TT2) → (TT1 -t> TT3) :=
   λ t1 t2, tele_bind (compose (tele_app t1) (tele_app t2)).
 
-Lemma tele_compose_eq {TT1 TT2 TT3 : tele} (f : TT2 -t> TT3) (g : TT1 -t> TT2) x :
-  tele_compose f g $ x = (f ∘ g) x.
-Proof. unfold tele_compose. rewrite tele_app_bind. done. Qed.
+Lemma tele_fun_compose_eq {TT1 TT2 TT3 : tele} (f : TT2 -t> TT3) (g : TT1 -t> TT2) x :
+  tele_fun_compose f g $ x = (f ∘ g) x.
+Proof. unfold tele_fun_compose. rewrite tele_app_bind. done. Qed.
 
 (** Notation *)
 Notation "'[tele' x .. z ]" :=
-- 
GitLab