From 8435606d98e418394edbe5104b3f425e56a5a207 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 31 Mar 2019 22:36:21 +0200
Subject: Generic.toList-fromList is Data.Vec.Properties.toList∘fromList
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Generic.agda | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'Generic.agda')

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