diff --git a/Language.agda b/Language.agda
index 473d218..b23e4a5 100644
--- a/Language.agda
+++ b/Language.agda
@@ -269,7 +269,9 @@ module Graphs where
                 ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns)
                 ; e∈g₁⇒e∈g₂ = λ {e} e∈es →
                     cast∈⇒∈subst (+-comm s 0) (+-comm 0 s) _ _
-                                 (subst (λ e' → e' ∈ˡ _) (↑ˡ-Edge-identityʳ e (+-comm s 0)) (∈ˡ-++⁺ʳ es' e∈es))
+                                 (subst (λ e' → e' ∈ˡ _)
+                                        (↑ˡ-Edge-identityʳ e (+-comm s 0))
+                                        (∈ˡ-++⁺ʳ es' e∈es))
                 }
             )