diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 548ad58a..6a46f4bb 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -737,11 +737,17 @@ count {∅}     _        =  ⊥-elim impossible
 ## Renaming
 
 ```
-ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
+ext : ∀ {Γ Δ}
+  → (∀ {A}   →     Γ ∋ A →     Δ ∋ A)
+    ---------------------------------
+  → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
 ext ρ Z      =  Z
 ext ρ (S x)  =  S (ρ x)
 
-rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+rename : ∀ {Γ Δ}
+  → (∀ {A} → Γ ∋ A → Δ ∋ A)
+    -----------------------
+  → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
 rename ρ (` x)          =  ` (ρ x)
 rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
 rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)