From 248dc87e7c282a56bcc13fc28701a572288bc3ec Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Mon, 17 Feb 2014 10:30:43 +0100
Subject: avoid useless repetition

---
 Bidir.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3