From 25bdb78f7f1bfc60b26d4febb213be5c4501cd6c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 28 Jun 2018 16:34:56 +0200
Subject: [PATCH] remove some redundant parentheses

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

diff --git a/theories/telescopes.v b/theories/telescopes.v
index 1a704fb8..6b7f5213 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -160,7 +160,7 @@ Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. ))
   format "∃..  x  ..  y ,  P") : stdpp_scope.
 
 Lemma tforall_forall {TT : tele} (Ψ : TT → Prop) :
-  (tforall Ψ) ↔ (∀ x, Ψ x).
+  tforall Ψ ↔ (∀ x, Ψ x).
 Proof.
   symmetry. unfold tforall. induction TT as [|X ft IH].
   - simpl. split.
@@ -173,7 +173,7 @@ Proof.
 Qed.
 
 Lemma texist_exist {TT : tele} (Ψ : TT → Prop) :
-  (texist Ψ) ↔ (ex Ψ).
+  texist Ψ ↔ ex Ψ.
 Proof.
   symmetry. induction TT as [|X ft IH].
   - simpl. split.
-- 
GitLab