From 4658c1e2759b6bfddbe3cc23bef1e8cbd6a3023c Mon Sep 17 00:00:00 2001
From: Jeremy Siek <jsiek@129-79-241-203.dhcp-bl.indiana.edu>
Date: Mon, 6 May 2019 15:01:34 +0200
Subject: [PATCH] minor tweak

---
 extra/extra/CallByName.lagda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/extra/extra/CallByName.lagda b/extra/extra/CallByName.lagda
index 6f5ac00a..e917fe9b 100644
--- a/extra/extra/CallByName.lagda
+++ b/extra/extra/CallByName.lagda
@@ -122,8 +122,7 @@ commute-subst-rename{Γ}{Δ}{ƛ N}{σ}{ρ} r = cong ƛ_ IH
    ρ' {∅} = λ ()
    ρ' {Γ , ★} = ext ρ
 
-   H : {x : Γ , ★ ∋ ★} →
-       exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
+   H : {x : Γ , ★ ∋ ★} → exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
    H {Z} = refl
    H {S x} =
      begin