diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index b161c25..4de15fb 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -215,9 +215,9 @@ module WithProg (prog : Program) where
 
             module WithValidity (interpretationValidˡ : InterpretationValid) where
 
-                updateVariablesFromStmt-matches : ∀ bs vs ρ₁ ρ₂ → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
-                updateVariablesFromStmt-matches _ vs ρ₁ ρ₁ (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
-                updateVariablesFromStmt-matches _ vs ρ₁ _ (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
+                updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
+                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
+                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
                     with k ≟ˢ k' | k',v'∈ρ₂
                 ...   | yes refl | here _ v _
                         rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =