use the indexed version of the Vec Setoid
[~helmut/bidiragda.git] / CheckInsert.agda
index 47af215..c8007ec 100644 (file)
@@ -18,7 +18,6 @@ import Relation.Binary.EqReasoning as EqR
 open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans)
 
 open import FinMap
-open import Generic using (vecIsSetoid)
 
 private
   open module A = DecSetoid A using (Carrier ; _≈_) renaming (_≟_ to deq)