1 files changed, 1 insertions, 1 deletions
diff --git a/Bidir.agda b/Bidir.agda
index f0b7bc1..fe3768d 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -248,4 +248,4 @@ theorem-2 G n s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid
           g′   = delete-many (get s′) g
           t    = enumeratel n
           h↦h′ = flip union (reshape g′ n)
-          h′↦r = flip mapMV (enumeratel n) ∘ flip lookupM
+          h′↦r = flip mapMV t ∘ flip lookupM