diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda
index d9921c5..df88452 100644
--- a/Analysis/Forward.agda
+++ b/Analysis/Forward.agda
@@ -247,6 +247,10 @@ module WithProg (prog : Program) where
                 in
                     ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
 
+            ⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
+                        ⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
+            ⟦⟧ᵛ-foldr = {!!}
+
             InterpretationValid : Set
             InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v