diff options
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 ⟩ |