Generic.toList-fromList is Data.Vec.Properties.toList∘fromList

2 files changed, 5 insertions, 8 deletions

diff --git a/Generic.agda b/Generic.agda
index 3106c5f..323688a 100644
--- a/Generic.agda
+++ b/Generic.agda
@@ -58,10 +58,6 @@ subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p′
               P.subst T p′ (P.subst T p x) ≡ P.subst T (P.trans p p′) x
 subst-subst T P.refl p′ x = P.refl
 
-toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l
-toList-fromList []L       = P.refl
-toList-fromList (x ∷L xs) = P.cong (_∷L_ x) (toList-fromList xs)
-
 toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) →
                toList (P.subst (Vec A) p v) ≡ toList v
 toList-subst v P.refl = P.refl
diff --git a/LiftGet.agda b/LiftGet.agda
index 9e2a805..4ddf26f 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -3,6 +3,7 @@ module LiftGet where
 open import Data.Unit using (⊤ ; tt)
 open import Data.Nat using (ℕ ; suc)
 open import Data.Vec using (Vec ; toList ; fromList) renaming ([] to []V ; _∷_ to _∷V_ ; map to mapV)
+open import Data.Vec.Properties using (toList∘fromList)
 open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
 open import Data.List.Properties using (length-map ; length-replicate)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
@@ -11,7 +12,7 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; pr
 open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable)
 
 import FreeTheorems
-open import Generic using (toList-fromList ; toList-subst)
+open import Generic using (toList-subst)
 open FreeTheorems.ListList using (get-type) renaming (free-theorem to free-theoremL ; Get to GetL ; module Get to GetL)
 open FreeTheorems.VecVec using () renaming (get-type to getV-type ; Get to GetV ; module Get to GetV)
 
@@ -114,7 +115,7 @@ GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft
 get-commut-1-≅ : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≅ proj₂ (getList-to-getVec get) (fromList l)
 get-commut-1-≅ get l = begin
   fromList (get l)
-    ≅⟨ H.cong (fromList ∘ get) (≡-to-≅ (P.sym (toList-fromList l))) ⟩
+    ≅⟨ H.cong (fromList ∘ get) (≡-to-≅ (P.sym (toList∘fromList l))) ⟩
   fromList (get (toList (fromList l)))
     ≅⟨ H.sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩
   P.subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎
@@ -138,9 +139,9 @@ get-trafo-1 get {B} l = begin
   toList (P.subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
     ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩
   toList (fromList (get (toList (fromList l))))
-    ≡⟨ toList-fromList (get (toList (fromList l))) ⟩
+    ≡⟨ toList∘fromList (get (toList (fromList l))) ⟩
   get (toList (fromList l))
-    ≡⟨ P.cong get (toList-fromList l) ⟩
+    ≡⟨ P.cong get (toList∘fromList l) ⟩
   get l ∎
   where open ≡-Reasoning