fix wrong function name in lemma-2

lookup and lookupM reference the same function, but serve different
purposes.

1 files changed, 1 insertions, 1 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 940a02d..163714a 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -80,7 +80,7 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h () | nothing | _
 lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | Reveal_is_.[_] ir = begin
   map (flip lookupM h) (i ∷ is)
     ≡⟨ refl ⟩
-  lookup i h ∷ map (flip lookupM h) is
+  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
       assoc eq (i ∷ is) (x ∷ xs)
         ≡⟨ cong (flip _>>=_ (checkInsert eq i x)) ir ⟩