From f0b0d51b488be7f4aab036bc8527ef4fd0734585 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Wed, 8 May 2024 23:38:23 -0700
Subject: [PATCH] Add unproven lemma about fold implication

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Analysis/Forward.agda | 4 ++++
 1 file changed, 4 insertions(+)

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