From c08be55fdd6802c83ad2e4ad679dae06b14fe5f9 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Sat, 26 Jul 2025 16:02:51 -0400
Subject: [PATCH] Removed rewrite that did nothing.

---
 src/plfa/part3/Soundness.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/plfa/part3/Soundness.lagda.md b/src/plfa/part3/Soundness.lagda.md
index 1c883f493..3d441fd0d 100644
--- a/src/plfa/part3/Soundness.lagda.md
+++ b/src/plfa/part3/Soundness.lagda.md
@@ -394,7 +394,7 @@ subst-reflect-var {Γ}{Δ}{γ}{x}{v}{σ} xv
   const-env-ok : γ `⊢ σ ↓ const-env x v
   const-env-ok y with x var≟ y
   ... | yes x≡y rewrite sym x≡y | same-const-env {Γ}{x}{v} = xv
-  ... | no x≢y rewrite diff-const-env {Γ}{x}{y}{v} x≢y = ⊥-intro
+  ... | no x≢y = ⊥-intro
 ```