Prove a property of multi-key lookup

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/FiniteMap.agda

@@ -30,6 +30,7 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
         ; ≈-dec to ≈ᵐ-dec
         ; _[_] to _[_]ᵐ
+        ; []-∈ to []ᵐ-∈
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
         ; locate to locateᵐ
         ; keys to keysᵐ
@@ -104,6 +105,10 @@ module WithKeys (ks : List A) where
     _[_] : FiniteMap → List A → List B
     _[_] (m₁ , _) ks = m₁ [ ks ]ᵐ
 
+    []-∈ : ∀ {k : A} {v : B} {ks' : List A} (fm : FiniteMap) →
+           k ∈ˡ ks' → (k , v) ∈ fm → v ∈ˡ (fm [ ks' ])
+    []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks' 
+
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
         { ≈-refl =

Lattice/Map.agda

@@ -1112,6 +1112,19 @@ _[_] m (k ∷ ks)
 ...   | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ])
 ...   | no _ = m [ ks ]
 
+[]-∈ : ∀ {k : A} {v : B} {ks : List A} (m : Map) →
+       (k , v) ∈ m → k ∈ˡ ks → v ∈ˡ (m [ ks ])
+[]-∈ {k} {v} {ks} m k,v∈m (here refl)
+    with ∈k-dec k (proj₁ m)
+...    | no k∉km = ⊥-elim (k∉km (forget k,v∈m))
+...    | yes k∈km
+         with (v' , k,v'∈m) ← locate {m = m} k∈km
+         rewrite Map-functional {m = m} k,v'∈m k,v∈m = here refl
+[]-∈ {k} {v} {k' ∷ ks'} m k,v∈m (there k∈ks')
+    with ∈k-dec k' (proj₁ m)
+...   | no _  = []-∈ m k,v∈m k∈ks'
+...   | yes _ = there ([]-∈ m k,v∈m k∈ks')
+
 m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (m₁ m₂ : Map) {k : A} {v₁ v₂ : B} →
                     m₁ ≼ m₂ → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → v₁ ≼₂ v₂
 m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂