cleanup unused functions and useless steps

1 files changed, 1 insertions, 9 deletions

diff --git a/Bidir.agda b/Bidir.agda
index eef8bff..05ee066 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -22,7 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨
 
 import FreeTheorems
 open FreeTheorems.VecVec using (get-type ; free-theorem)
-open import Generic using (just-injective ; map-just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
+open import Generic using (just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
 open import FinMap
 import CheckInsert
 open CheckInsert Carrier deq
@@ -150,14 +150,6 @@ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma
 lemma->>=-just (just a) p = a , refl
 lemma->>=-just nothing  ()
 
-lemma-mapMV-just : {A B : Set} {n : ℕ} {f : A → Maybe B} {s : Vec A n} {v : Vec B n} → mapMV f s ≡ just v → All (λ x → ∃ λ y → f x ≡ just y) (toList s)
-lemma-mapMV-just         {s = []}     p = Data.List.All.[]
-lemma-mapMV-just {f = f} {s = x ∷ xs} p with f x | inspect f x
-lemma-mapMV-just         {s = x ∷ xs} () | nothing | _
-lemma-mapMV-just {f = f} {s = x ∷ xs} p  | just y  | [ py ] with mapMV f xs | inspect (mapMV f) xs
-lemma-mapMV-just         {s = x ∷ xs} () | just y  | [ py ] | nothing | _
-lemma-mapMV-just         {s = x ∷ xs} p  | just y  | [ py ] | just ys | [ pys ] = (y , py) Data.List.All.∷ (lemma-mapMV-just pys)
-
 lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
 lemma-just-sequence [] = refl
 lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl