From ddb751df76c004d788ed09c3ed54c562c99afb7b Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Fri, 27 Apr 2012 20:53:05 +0200
Subject: lemma-2: do not confuse lookup with lookupM

Even though they are the same.
---
 Bidir.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index f481eea..495fb99 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -232,7 +232,7 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | Reveal_is_.[_] ir = begin
   map (flip lookupM h) (i ∷ is)
     ≡⟨ refl ⟩
   lookupM i h ∷ map (flip lookupM h) is
-    ≡⟨ cong (flip _∷_ (map (flip lookup h) is)) (lemma-lookupM-assoc eq i is x xs h (begin
+    ≡⟨ cong (flip _∷_ (map (flip lookupM h) is)) (lemma-lookupM-assoc eq i is x xs h (begin
       assoc eq (i ∷ is) (x ∷ xs)
         ≡⟨ cong (flip _>>=_ (checkInsert eq i x)) ir ⟩
       checkInsert eq i x h'
-- 
cgit v1.2.3