From 4119cde3c86e55e23f8fe83a550e99a993acc5e3 Mon Sep 17 00:00:00 2001
From: Reza Gharibi <reza.gharibi.rg@gmail.com>
Date: Wed, 19 Jun 2019 18:41:01 +0430
Subject: [PATCH] Removed a redundant sentence

---
 src/plfa/DeBruijn.lagda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/plfa/DeBruijn.lagda b/src/plfa/DeBruijn.lagda
index 5d9032f5..abc8eecd 100644
--- a/src/plfa/DeBruijn.lagda
+++ b/src/plfa/DeBruijn.lagda
@@ -360,8 +360,7 @@ data _⊢_ : Context → Type → Set where
 The definition exploits the close correspondence between the
 structure of terms and the structure of a derivation showing
 that it is well-typed: now we use the derivation _as_ the
-term.  For example, consider the following three terms,
-building up the Church numeral two.
+term.
 
 For example, consider the following old-style typing
 judgments: