Prove things about key-based access in map

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

Lattice/Map.agda

@@ -1086,3 +1086,29 @@ module _ {l} {L : Set l}
                             with refl ← Map-functional {m = f' l₂} k,v∈f'l₂ k,v₂∈f'l₂
                             with refl ← Map-functional {m = f l₂} k,v'∈fl₂ k,v₂∈fl₂ =
                             (v₁ ⊔₂ v , (v'≈v'' , k,v₁v₂∈f'l₁f'l₂))
+
+
+_[_] : Map → List A → List B
+_[_] m [] = []
+_[_] m (k ∷ ks)
+    with ∈k-dec k (proj₁ m)
+...   | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ])
+...   | no _ = m [ 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₂
+    with k,v₁v₂∈m₁m₂ ← ⊔-combines {m₁ = m₁} {m₂ = m₂} k,v₁∈m₁ k,v₂∈m₂
+    with (v' , (v₁v₂≈v' , k,v'∈m₂)) ← (proj₁ m₁≼m₂) _ _ k,v₁v₂∈m₁m₂
+    with refl ← Map-functional {m = m₂} k,v₂∈m₂ k,v'∈m₂
+    = v₁v₂≈v'
+
+m₁≼m₂⇒k∈km₁⇒k∈km₂ : ∀ (m₁ m₂ : Map) {k : A} →
+                    m₁ ≼ m₂ → k ∈k m₁ → k ∈k m₂
+m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
+    let
+        k∈km₁m₂ = union-preserves-∈k₁ {l₁ = proj₁ m₁} {l₂ = proj₁ m₂} k∈km₁
+        (v , k,v∈m₁m₂) = locate {m = m₁ ⊔ m₂} k∈km₁m₂
+        (v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
+    in
+        forget k,v'∈m₂