Successfully prove that monotonic updates preserve existing indices

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

Language.agda

@@ -179,6 +179,14 @@ module Graphs where
                 )
             }
 
+    open Relaxable {{...}} public
+
+    relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
+                          g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
+    relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl g₁[]≡g₂[] _) idx =
+        trans (g₁[]≡g₂[] idx) (cong (λ vec → lookup vec (idx ↑ˡ n))
+                                    (cast-is-id refl (Graph.nodes g₂)))
+
     MonotonicGraphFunction : (Graph → Set) → Set
     MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
 
@@ -259,8 +267,6 @@ module Graphs where
                       addEdges g ((idx , idx') ∷ (idx₂ , idx) ∷ []) })
             map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') })
 
-    -- open Relaxable {{...}} public
-
 open import Lattice.MapSet _≟ˢ_
     renaming
         ( MapSet to StringSet