diff --git a/Language.agda b/Language.agda
index b23e4a5..4c495d3 100644
--- a/Language.agda
+++ b/Language.agda
@@ -104,12 +104,26 @@ module Graphs where
             nodes : Vec (List BasicStmt) size
             edges : List Edge
 
-    castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m)
-    castᵉ p (idx₁ , idx₂) = (castᶠ p idx₁ , castᶠ p idx₂)
-
     ↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n +ⁿ m) × Fin (n +ⁿ m))
     ↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m)
 
+    _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
+    _[_] g idx = lookup (Graph.nodes g) idx
+
+    record _⊆_ (g₁ g₂ : Graph) : Set where
+        constructor Mk-⊆
+        field
+            n : ℕ
+            sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
+            newNodes : Vec (List BasicStmt) n
+            nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes
+            e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} →
+                        e ∈ˡ (Graph.edges g₁) →
+                        (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
+
+    castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m)
+    castᵉ p (idx₁ , idx₂) = (castᶠ p idx₁ , castᶠ p idx₂)
+
     ↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s +ⁿ (n₁ +ⁿ n₂) ≡ s +ⁿ n₁ +ⁿ n₂) →
                f ↑ˡ n₁ ↑ˡ n₂ ≡ castᶠ p (f ↑ˡ (n₁ +ⁿ n₂))
     ↑ˡ-assoc zero p = refl
@@ -140,20 +154,6 @@ module Graphs where
         rewrite castᶠ-is-id refl idx₁
         rewrite castᶠ-is-id refl idx₂ = e∈es
 
-    _[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
-    _[_] g idx = lookup (Graph.nodes g) idx
-
-    record _⊆_ (g₁ g₂ : Graph) : Set where
-        constructor Mk-⊆
-        field
-            n : ℕ
-            sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
-            newNodes : Vec (List BasicStmt) n
-            nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes
-            e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} →
-                        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 newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂)