diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index 678bccc..5d0458a 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -356,8 +356,6 @@ module WithProg (prog : Program) where
                     in
                         walkTrace ⟦joinForKey-s⟧ρ tr
 
-                postulate initialState-pred-∅ : incoming initialState ≡ []
-
                 joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
                 joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
 
diff --git a/Language.agda b/Language.agda
index 1c88ba8..5d54048 100644
--- a/Language.agda
+++ b/Language.agda
@@ -84,6 +84,10 @@ record Program : Set where
     incoming : State → List State
     incoming = predecessors graph
 
+    initialState-pred-∅ : incoming initialState ≡ []
+    initialState-pred-∅ =
+        wrap-preds-∅ (buildCfg rootStmt) initialState (RelAny.here refl)
+
     edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
                     s₁ ListMem.∈ (incoming s₂)
     edge⇒incoming = edge⇒predecessor graph