lemma-2: do not confuse lookup with lookupM
authorHelmut Grohne <helmut@subdivi.de>
Fri, 27 Apr 2012 18:53:05 +0000 (20:53 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 27 Apr 2012 18:53:05 +0000 (20:53 +0200)
Even though they are the same.

Bidir.agda

index f481eea..495fb99 100644 (file)
@@ -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'