From 40b63478babed534ef74a594a99a428ffc5b232d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Crist=C3=B3v=C3=A3o=20Gomes=20Ferreira=20=28Melo=20Gibson?=
 =?UTF-8?q?=29?= <crisoagf@melo-gibson>
Date: Thu, 3 Dec 2020 20:14:48 +0000
Subject: [PATCH] =?UTF-8?q?547=20-=20Proving=20trans=20using=20=E2=89=A1-R?=
 =?UTF-8?q?easoning=20is=20circular?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/plfa/part1/Equality.lagda.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/plfa/part1/Equality.lagda.md b/src/plfa/part1/Equality.lagda.md
index 84653fbd..cf08b76b 100644
--- a/src/plfa/part1/Equality.lagda.md
+++ b/src/plfa/part1/Equality.lagda.md
@@ -268,6 +268,14 @@ simplifies to a chain of applications of `trans` that ends in `trans e
 refl`, where `e` is a term that proves some equality, even though `e`
 alone would do.
 
+#### Exercise `trans` and `≡-Reasoning` (practice)
+
+Sadly, we cannot use the definition of trans' using ≡-Reasoning as the definition
+for trans. Can you see why? (Hint: look at the definition of `_≡⟨_⟩_`)
+
+```
+-- Your code goes here
+```
 
 ## Chains of equations, another example