cleanup unused function and import

1 files changed, 1 insertions, 5 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 32d0ae7..838df25 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -25,7 +25,7 @@ import Relation.Binary.EqReasoning as EqR
 
 import FreeTheorems
 open FreeTheorems.VecVec using (get-type ; free-theorem)
-open import Generic using (just-injective ; vecIsSetoid ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
+open import Generic using (vecIsSetoid ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
 open import FinMap
 import CheckInsert
 open CheckInsert A
@@ -170,10 +170,6 @@ lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = congβ‚
   (lemma-union-not-used h h' is' p')
   where open ≑-Reasoning
 
-map-just-β‰ˆ-injective : {n : β„•} {x y : Vec Carrier n} β†’ Setoid._β‰ˆ_ (vecIsSetoid (MaybeSetoid A.setoid) n) (map just x) (map just y) β†’ Setoid._β‰ˆ_ (vecIsSetoid A.setoid n) x y
-map-just-β‰ˆ-injective {x = []}    {y = []}    VecEq.[]-cong              = VecEq.[]-cong
-map-just-β‰ˆ-injective {x = _ ∷ _} {y = _ ∷ _} (just xβ‰ˆy VecEq.∷-cong ps) = xβ‰ˆy VecEq.∷-cong map-just-β‰ˆ-injective ps
-
 lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A β†’ Maybe B} {b : B} β†’ (ma >>= f) ≑ just b β†’ βˆƒ Ξ» a β†’ ma ≑ just a
 lemma->>=-just (just a) p = a , refl
 lemma->>=-just nothing  ()