From b863e05247453f8a55930df5c061c156158eab0c Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Fri, 14 Sep 2012 17:23:58 +0200
Subject: vec-len-via-list and length-toList are the same

---
 LiftGet.agda | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/LiftGet.agda b/LiftGet.agda
index c3c5294..d4e7d9f 100644
--- a/LiftGet.agda
+++ b/LiftGet.agda
@@ -105,10 +105,6 @@ get-trafo-1 get {B} l = begin
 vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
 vec-len {_} {n} _ = n
 
-vec-len-via-list : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ vec-len v
-vec-len-via-list []V       = refl
-vec-len-via-list (x ∷V xs) = cong suc (vec-len-via-list xs)
-
 length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
 length-replicate 0       = refl
 length-replicate (suc n) = cong suc (length-replicate n)
@@ -145,7 +141,7 @@ get-trafo-2-getlen getlen get n = begin
   proj₁ (getList-to-getVec (getVec-to-getList get)) n
     ≡⟨ refl ⟩
   length (toList (get (fromList (replicate n tt))))
-    ≡⟨ vec-len-via-list (get (fromList (replicate n tt))) ⟩
+    ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩
   vec-len (get (fromList (replicate n tt)))
     ≡⟨ cong getlen (length-replicate n) ⟩
   getlen n ∎
-- 
cgit v1.2.3