diff --git a/Language.agda b/Language.agda
index e769597..979fcec 100644
--- a/Language.agda
+++ b/Language.agda
@@ -228,7 +228,7 @@ module Graphs where
               , record
                   { n = 1
                   ; sg₂≡sg₁+n = refl
-                  ; g₁[]≡g₂[] = λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ [])))))
+                  ; g₁[]≡g₂[] = {!!} -- λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ [])))))
                   ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁
                   }
               )