diff --git a/Language.agda b/Language.agda
index 2b078d9..3b593fc 100644
--- a/Language.agda
+++ b/Language.agda
@@ -134,7 +134,8 @@ module Graphs where
             (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record
         { n = n₁ +ⁿ n₂
         ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
-        -- ; g₁[]≡g₂[] = λ idx → 1
+        ; g₁[]≡g₂[] = {!!}
+        ; e∈g₁⇒e∈g₂ = {!!}
         --     lookup ns₁ idx ≡ lookup (cast p₁ ns₂) (idx ↑ˡ n) -- by g₁[]≡g₂[]
 
         --     lookup (cast p₁ ns₂) (idx ↑ˡ n) ≡ lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) -- by lookup-cast₁