diff --git a/Language.agda b/Language.agda
index 725c4f2..99a7737 100644
--- a/Language.agda
+++ b/Language.agda
@@ -3,6 +3,7 @@ module Language where
 open import Language.Base public
 open import Language.Semantics public
 open import Language.Graphs public
+open import Language.Properties public
 
 open import Data.Fin using (Fin; suc; zero)
 open import Data.Fin.Properties as FinProp using (suc-injective)
diff --git a/Language/Graphs.agda b/Language/Graphs.agda
index a594740..022eaba 100644
--- a/Language/Graphs.agda
+++ b/Language/Graphs.agda
@@ -1,7 +1,6 @@
 module Language.Graphs where
 
 open import Language.Base
-open import Language.Semantics
 
 open import Data.Fin as Fin using (Fin; suc; zero; _↑ˡ_; _↑ʳ_)
 open import Data.Fin.Properties as FinProp using (suc-injective)
@@ -57,38 +56,39 @@ record _⊆_ (g₁ g₂ : Graph) : Set where
                     e ListMem.∈ (Graph.edges g₁) →
                     (↑ˡ-Edge e n) ListMem.∈ (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₂) = (Fin.cast p idx₁ , Fin.cast p idx₂)
+private
+    castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m)
+    castᵉ p (idx₁ , idx₂) = (Fin.cast p idx₁ , Fin.cast p idx₂)
 
-↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) →
-           f ↑ˡ n₁ ↑ˡ n₂ ≡ Fin.cast p (f ↑ˡ (n₁ Nat.+ n₂))
-↑ˡ-assoc zero p = refl
-↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl
+    ↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) →
+               f ↑ˡ n₁ ↑ˡ n₂ ≡ Fin.cast p (f ↑ˡ (n₁ Nat.+ n₂))
+    ↑ˡ-assoc zero p = refl
+    ↑ˡ-assoc {suc s'} {n₁} {n₂} (suc f') p rewrite ↑ˡ-assoc f' (sym (+-assoc s' n₁ n₂)) = refl
 
-↑ˡ-Edge-assoc : ∀ {s n₁ n₂} (e : Fin s × Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) →
-                ↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ ≡ castᵉ p (↑ˡ-Edge e (n₁ Nat.+ n₂))
-↑ˡ-Edge-assoc (idx₁ , idx₂) p
-    rewrite ↑ˡ-assoc idx₁ p
-    rewrite ↑ˡ-assoc idx₂ p = refl
+    ↑ˡ-Edge-assoc : ∀ {s n₁ n₂} (e : Fin s × Fin s) (p : s Nat.+ (n₁ Nat.+ n₂) ≡ s Nat.+ n₁ Nat.+ n₂) →
+                    ↑ˡ-Edge (↑ˡ-Edge e n₁) n₂ ≡ castᵉ p (↑ˡ-Edge e (n₁ Nat.+ n₂))
+    ↑ˡ-Edge-assoc (idx₁ , idx₂) p
+        rewrite ↑ˡ-assoc idx₁ p
+        rewrite ↑ˡ-assoc idx₂ p = refl
 
-↑ˡ-identityʳ : ∀ {s} (f : Fin s) (p : s Nat.+ 0 ≡ s) →
-           f ≡ Fin.cast p (f ↑ˡ 0)
-↑ˡ-identityʳ zero p = refl
-↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl
+    ↑ˡ-identityʳ : ∀ {s} (f : Fin s) (p : s Nat.+ 0 ≡ s) →
+               f ≡ Fin.cast p (f ↑ˡ 0)
+    ↑ˡ-identityʳ zero p = refl
+    ↑ˡ-identityʳ {suc s'} (suc f') p rewrite sym (↑ˡ-identityʳ f' (+-comm s' 0)) = refl
 
-↑ˡ-Edge-identityʳ : ∀ {s} (e : Fin s × Fin s) (p : s Nat.+ 0 ≡ s) →
-                    e ≡ castᵉ p (↑ˡ-Edge e 0)
-↑ˡ-Edge-identityʳ (idx₁ , idx₂) p
-    rewrite sym (↑ˡ-identityʳ idx₁ p)
-    rewrite sym (↑ˡ-identityʳ idx₂ p) = refl
+    ↑ˡ-Edge-identityʳ : ∀ {s} (e : Fin s × Fin s) (p : s Nat.+ 0 ≡ s) →
+                        e ≡ castᵉ p (↑ˡ-Edge e 0)
+    ↑ˡ-Edge-identityʳ (idx₁ , idx₂) p
+        rewrite sym (↑ˡ-identityʳ idx₁ p)
+        rewrite sym (↑ˡ-identityʳ idx₂ p) = refl
 
-cast∈⇒∈subst : ∀ {n m : ℕ} (p : n ≡ m) (q : m ≡ n)
-               (e : Fin n × Fin n) (es : List (Fin m × Fin m)) →
-               castᵉ p e ListMem.∈ es →
-               e ListMem.∈ subst (λ m → List (Fin m × Fin m)) q es
-cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
-    rewrite FinProp.cast-is-id refl idx₁
-    rewrite FinProp.cast-is-id refl idx₂ = e∈es
+    cast∈⇒∈subst : ∀ {n m : ℕ} (p : n ≡ m) (q : m ≡ n)
+                   (e : Fin n × Fin n) (es : List (Fin m × Fin m)) →
+                   castᵉ p e ListMem.∈ es →
+                   e ListMem.∈ subst (λ m → List (Fin m × Fin m)) q es
+    cast∈⇒∈subst refl refl (idx₁ , idx₂) es e∈es
+        rewrite FinProp.cast-is-id refl idx₁
+        rewrite FinProp.cast-is-id refl idx₂ = e∈es
 
 ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
 ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
@@ -128,20 +128,6 @@ instance
 
 open Relaxable {{...}}
 
-relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
-                      g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
-relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNodes _) idx
-    rewrite cast-is-id refl (Graph.nodes g₂)
-    with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _)
-
-instance
-    NodeEqualsMonotonic : ∀ {bss : List BasicStmt} →
-                          MonotonicPredicate (λ g n → g [ n ] ≡ bss)
-    NodeEqualsMonotonic = record
-        { relaxPredicate = λ g₁ g₂ idx g₁⊆g₂ g₁[idx]≡bss →
-            trans (sym (relax-preserves-[]≡ g₁ g₂ g₁⊆g₂ idx)) g₁[idx]≡bss
-        }
-
 pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
 pushBasicBlock bss g =
     ( record
@@ -160,8 +146,8 @@ pushBasicBlock bss g =
       )
     )
 
-pushBasicBlock-works : ∀ (bss : List BasicStmt) → Always (λ g idx → g [ idx ] ≡ bss) (pushBasicBlock bss)
-pushBasicBlock-works bss = MkAlways (λ g → lookup-++ʳ (Graph.nodes g) (bss ∷ []) zero)
+pushEmptyBlock : MonotonicGraphFunction Graph.Index
+pushEmptyBlock = pushBasicBlock []
 
 addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
 addEdges (MkGraph s ns es) es' =
@@ -183,9 +169,6 @@ addEdges (MkGraph s ns es) es' =
         }
     )
 
-pushEmptyBlock : MonotonicGraphFunction Graph.Index
-pushEmptyBlock = pushBasicBlock []
-
 buildCfg : Stmt → MonotonicGraphFunction (Graph.Index ⊗ Graph.Index)
 buildCfg ⟨ bs₁ ⟩ = pushBasicBlock (bs₁ ∷ []) map (λ g idx → (idx , idx))
 buildCfg (s₁ then s₂) =
diff --git a/Language/Properties.agda b/Language/Properties.agda
new file mode 100644
index 0000000..c5dea39
--- /dev/null
+++ b/Language/Properties.agda
@@ -0,0 +1,31 @@
+module Language.Properties where
+
+open import Language.Base
+open import Language.Semantics
+open import Language.Graphs
+
+open import MonotonicState _⊆_ ⊆-trans renaming (MonotonicState to MonotonicGraphFunction)
+open Relaxable {{...}}
+
+open import Data.Fin using (zero)
+open import Data.List using (List)
+open import Data.Vec using (_∷_; [])
+open import Data.Vec.Properties using (cast-is-id; lookup-++ˡ; lookup-++ʳ)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
+
+relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
+                      g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
+relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNodes _) idx
+    rewrite cast-is-id refl (Graph.nodes g₂)
+    with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _)
+
+instance
+    NodeEqualsMonotonic : ∀ {bss : List BasicStmt} →
+                          MonotonicPredicate (λ g n → g [ n ] ≡ bss)
+    NodeEqualsMonotonic = record
+        { relaxPredicate = λ g₁ g₂ idx g₁⊆g₂ g₁[idx]≡bss →
+            trans (sym (relax-preserves-[]≡ g₁ g₂ g₁⊆g₂ idx)) g₁[idx]≡bss
+        }
+
+pushBasicBlock-works : ∀ (bss : List BasicStmt) → Always (λ g idx → g [ idx ] ≡ bss) (pushBasicBlock bss)
+pushBasicBlock-works bss = MkAlways (λ g → lookup-++ʳ (Graph.nodes g) (bss ∷ []) zero)