diff --git a/Language.agda b/Language.agda
index f440aba..d2af0dc 100644
--- a/Language.agda
+++ b/Language.agda
@@ -121,10 +121,25 @@ module Graphs where
                         e ∈ˡ (Graph.edges g₁) →
                         (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
 
+
     ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
-    ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃} (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record
+    ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
+            (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
+        --     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₁
+        --                                                            -------- s₁ + n₁ → s₂
+        --                                                                     ---------- Fin (s₁ + n₁)
+        --                                                  ----------------------------- Fin s₂
+
+        --     lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) ≡ lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂)) -- by g₂[]≡g₃[]
+
+        --     lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ  n₂)) ≡ lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ  n₂))) -- by lookup-cast₂
+
+        --     -- ??
         }
 
     record Relaxable (T : Graph → Set) : Set where