Actually force proof of 'analyze-correct'

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

Analysis/Forward.agda

@@ -8,6 +8,7 @@ module Analysis.Forward
     {{≈ˡ-dec : IsDecidable _≈ˡ_}} where
 
 open import Data.Empty using (⊥-elim)
+open import Data.Unit using (⊤)
 open import Data.String using (String)
 open import Data.Product using (_,_)
 open import Data.List using (_∷_; []; foldr; foldl)
@@ -77,7 +78,7 @@ module WithProg (prog : Program) where
             updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
 
         module WithValidInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
-                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} where
+                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} (dummy : ⊤) where
             open ValidStmtEvaluator validEvaluator
 
             eval-fold-valid : ∀ {s bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip (eval s)) vs bss ⟧ᵛ ρ₂