From 99020536803dd83e0d3c2cce14728579c9b0ae63 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= <marko@dimjasevic.net>
Date: Wed, 30 Jan 2019 16:24:30 +0100
Subject: [PATCH] Connectives: fixes an explanation of simplification

---
 src/plfa/Connectives.lagda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda
index d84b1119..64f04264 100644
--- a/src/plfa/Connectives.lagda
+++ b/src/plfa/Connectives.lagda
@@ -378,8 +378,8 @@ uniq-⊎ h (inj₁ x) = refl
 uniq-⊎ h (inj₂ y) = refl
 \end{code}
 The pattern matching on the left-hand side is essential.  Replacing
-`w` by `inj₁ x` allows both sides of the equation to simplify to the
-same term, and similarly for `inj₂ y`.
+`w` by `inj₁ x` allows both sides of the propositional equality to
+simplify to the same term, and similarly for `inj₂ y`.
 
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator: