diff --git a/CHANGELOG.md b/CHANGELOG.md
index bf625ae348..09bcea84cb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -531,6 +531,14 @@ Deprecated names
   idIsFold        ↦ id-is-foldr
   sum-++-commute  ↦ sum-++
   ```
+  and the type of the proof `zipWith-comm` has been generalised from:
+  ```
+  zipWith-comm : ∀ {f : A → A → B} (comm : ∀ x y → f x y ≡ f y x) (xs ys : Vec A n) → zipWith f xs ys ≡ zipWith f ys xs
+  ```
+  to
+  ```
+  zipWith-comm : ∀ {f : A → B → C} {g : B → A → C}  (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys → zipWith f xs ys ≡ zipWith g ys xs
+  ```
 
 * In `Function.Construct.Composition`:
   ```
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 8e92d64714..2554d488db 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -26,6 +26,7 @@ private
     A : Set a
     B : Set b
     C : Set c
+    m n : ℕ
 
 ------------------------------------------------------------------------
 -- Types
@@ -34,40 +35,40 @@ infixr 5 _∷_
 
 data Vec (A : Set a) : ℕ → Set a where
   []  : Vec A zero
-  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
+  _∷_ : ∀ (x : A) (xs : Vec A n) → Vec A (suc n)
 
 infix 4 _[_]=_
 
-data _[_]=_ {A : Set a} : ∀ {n} → Vec A n → Fin n → A → Set a where
-  here  : ∀ {n}     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
-  there : ∀ {n} {i} {x y} {xs : Vec A n}
-          (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x
+data _[_]=_ {A : Set a} : Vec A n → Fin n → A → Set a where
+  here  : ∀     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
+  there : ∀ {i} {x y} {xs : Vec A n}
+    (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x
 
 ------------------------------------------------------------------------
 -- Basic operations
 
-length : ∀ {n} → Vec A n → ℕ
+length : Vec A n → ℕ
 length {n = n} _ = n
 
-head : ∀ {n} → Vec A (1 + n) → A
+head : Vec A (1 + n) → A
 head (x ∷ xs) = x
 
-tail : ∀ {n} → Vec A (1 + n) → Vec A n
+tail : Vec A (1 + n) → Vec A n
 tail (x ∷ xs) = xs
 
-lookup : ∀ {n} → Vec A n → Fin n → A
+lookup : Vec A n → Fin n → A
 lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
 
-insert : ∀ {n} → Vec A n → Fin (suc n) → A → Vec A (suc n)
+insert : Vec A n → Fin (suc n) → A → Vec A (suc n)
 insert xs       zero     v = v ∷ xs
 insert (x ∷ xs) (suc i)  v = x ∷ insert xs i v
 
-remove : ∀ {n} → Vec A (suc n) → Fin (suc n) → Vec A n
+remove : Vec A (suc n) → Fin (suc n) → Vec A n
 remove (_ ∷ xs)     zero     = xs
 remove (x ∷ y ∷ xs) (suc i)  = x ∷ remove (y ∷ xs) i
 
-updateAt : ∀ {n} → Fin n → (A → A) → Vec A n → Vec A n
+updateAt : Fin n → (A → A) → Vec A n → Vec A n
 updateAt zero    f (x ∷ xs) = f x ∷ xs
 updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs
 
@@ -75,20 +76,20 @@ updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs
 
 infixl 6 _[_]%=_
 
-_[_]%=_ : ∀ {n} → Vec A n → Fin n → (A → A) → Vec A n
+_[_]%=_ : Vec A n → Fin n → (A → A) → Vec A n
 xs [ i ]%= f = updateAt i f xs
 
 -- xs [ i ]≔ y  overwrites the i-th element of xs with y
 
 infixl 6 _[_]≔_
 
-_[_]≔_ : ∀ {n} → Vec A n → Fin n → A → Vec A n
+_[_]≔_ : Vec A n → Fin n → A → Vec A n
 xs [ i ]≔ y = xs [ i ]%= const y
 
 ------------------------------------------------------------------------
 -- Operations for transforming vectors
 
-map : ∀ {n} → (A → B) → Vec A n → Vec B n
+map : (A → B) → Vec A n → Vec B n
 map f []       = []
 map f (x ∷ xs) = f x ∷ map f xs
 
@@ -96,51 +97,51 @@ map f (x ∷ xs) = f x ∷ map f xs
 
 infixr 5 _++_
 
-_++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
+_++_ : Vec A m → Vec A n → Vec A (m + n)
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
 
-concat : ∀ {m n} → Vec (Vec A m) n → Vec A (n * m)
+concat : Vec (Vec A m) n → Vec A (n * m)
 concat []         = []
 concat (xs ∷ xss) = xs ++ concat xss
 
 -- Align, Restrict, and Zip.
 
-alignWith : ∀ {m n} → (These A B → C) → Vec A m → Vec B n → Vec C (m ⊔ n)
+alignWith : (These A B → C) → Vec A m → Vec B n → Vec C (m ⊔ n)
 alignWith f []         bs       = map (f ∘′ that) bs
 alignWith f as@(_ ∷ _) []       = map (f ∘′ this) as
 alignWith f (a ∷ as)   (b ∷ bs) = f (these a b) ∷ alignWith f as bs
 
-restrictWith : ∀ {m n} → (A → B → C) → Vec A m → Vec B n → Vec C (m ⊓ n)
+restrictWith : (A → B → C) → Vec A m → Vec B n → Vec C (m ⊓ n)
 restrictWith f []       bs       = []
 restrictWith f (_ ∷ _)  []       = []
 restrictWith f (a ∷ as) (b ∷ bs) = f a b ∷ restrictWith f as bs
 
-zipWith : ∀ {n} → (A → B → C) → Vec A n → Vec B n → Vec C n
+zipWith : (A → B → C) → Vec A n → Vec B n → Vec C n
 zipWith f []       []       = []
 zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
 
-unzipWith : ∀ {n} → (A → B × C) → Vec A n → Vec B n × Vec C n
+unzipWith : (A → B × C) → Vec A n → Vec B n × Vec C n
 unzipWith f []       = [] , []
 unzipWith f (a ∷ as) = Prod.zip _∷_ _∷_ (f a) (unzipWith f as)
 
-align : ∀ {m n} → Vec A m → Vec B n → Vec (These A B) (m ⊔ n)
+align : Vec A m → Vec B n → Vec (These A B) (m ⊔ n)
 align = alignWith id
 
-restrict : ∀ {m n} → Vec A m → Vec B n → Vec (A × B) (m ⊓ n)
+restrict : Vec A m → Vec B n → Vec (A × B) (m ⊓ n)
 restrict = restrictWith _,_
 
-zip : ∀ {n} → Vec A n → Vec B n → Vec (A × B) n
+zip : Vec A n → Vec B n → Vec (A × B) n
 zip = zipWith _,_
 
-unzip : ∀ {n} → Vec (A × B) n → Vec A n × Vec B n
+unzip : Vec (A × B) n → Vec A n × Vec B n
 unzip = unzipWith id
 
 -- Interleaving.
 
 infixr 5 _⋎_
 
-_⋎_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m +⋎ n)
+_⋎_ : Vec A m → Vec A n → Vec A (m +⋎ n)
 []       ⋎ ys = ys
 (x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)
 
@@ -148,7 +149,7 @@ _⋎_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m +⋎ n)
 
 infixl 4 _⊛_
 
-_⊛_ : ∀ {n} → Vec (A → B) n → Vec A n → Vec B n
+_⊛_ : Vec (A → B) n → Vec A n → Vec B n
 []       ⊛ []       = []
 (f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)
 
@@ -157,27 +158,27 @@ _⊛_ : ∀ {n} → Vec (A → B) n → Vec A n → Vec B n
 module CartesianBind where
   infixl 1 _>>=_
 
-  _>>=_ : ∀ {m n} → Vec A m → (A → Vec B n) → Vec B (m * n)
+  _>>=_ : Vec A m → (A → Vec B n) → Vec B (m * n)
   xs >>= f = concat (map f xs)
 
 infixl 4 _⊛*_
 
-_⊛*_ : ∀ {m n} → Vec (A → B) m → Vec A n → Vec B (m * n)
+_⊛*_ : Vec (A → B) m → Vec A n → Vec B (m * n)
 fs ⊛* xs = fs CartesianBind.>>= λ f → map f xs
 
-allPairs : ∀ {m n} → Vec A m → Vec B n → Vec (A × B) (m * n)
+allPairs : Vec A m → Vec B n → Vec (A × B) (m * n)
 allPairs xs ys = map _,_ xs ⊛* ys
 
 -- Diagonal
 
-diagonal : ∀ {n} → Vec (Vec A n) n → Vec A n
+diagonal : Vec (Vec A n) n → Vec A n
 diagonal [] = []
 diagonal (xs ∷ xss) = head xs ∷ diagonal (map tail xss)
 
 module DiagonalBind where
   infixl 1 _>>=_
 
-  _>>=_ : ∀ {n} → Vec A n → (A → Vec B n) → Vec B n
+  _>>=_ : Vec A n → (A → Vec B n) → Vec B n
   xs >>= f = diagonal (map f xs)
 
 ------------------------------------------------------------------------
@@ -190,43 +191,37 @@ module _ (A : Set a) (B : ℕ → Set b) where
   FoldrOp = ∀ {n} → A → B n → B (suc n)
   FoldlOp = ∀ {n} → B n → A → B (suc n)
 
-foldr : ∀ (B : ℕ → Set b) {m} →
-        FoldrOp A B →
-        B zero →
-        Vec A m → B m
-foldr B _⊕_ n []       = n
-foldr B _⊕_ n (x ∷ xs) = x ⊕ foldr B _⊕_ n xs
+foldr : ∀ (B : ℕ → Set b) → FoldrOp A B → B zero → Vec A n → B n
+foldr B _⊕_ e []       = e
+foldr B _⊕_ e (x ∷ xs) = x ⊕ foldr B _⊕_ e xs
 
-foldl : ∀ (B : ℕ → Set b) {m} →
-        FoldlOp A B →
-        B zero →
-        Vec A m → B m
-foldl B _⊕_ n []       = n
-foldl B _⊕_ n (x ∷ xs) = foldl (B ∘ suc) _⊕_ (n ⊕ x) xs
+foldl : ∀ (B : ℕ → Set b) → FoldlOp A B → B zero → Vec A n → B n
+foldl B _⊕_ e []       = e
+foldl B _⊕_ e (x ∷ xs) = foldl (B ∘ suc) _⊕_ (e ⊕ x) xs
 
 -- Non-dependent folds
 
-foldr′ : ∀ {n} → (A → B → B) → B → Vec A n → B
-foldr′ _⊕_ = foldr _ λ {n} → _⊕_
+foldr′ : (A → B → B) → B → Vec A n → B
+foldr′ _⊕_ = foldr _ _⊕_
 
-foldl′ : ∀ {n} → (B → A → B) → B → Vec A n → B
-foldl′ _⊕_ = foldl _ λ {n} → _⊕_
+foldl′ : (B → A → B) → B → Vec A n → B
+foldl′ _⊕_ = foldl _ _⊕_
 
 -- Non-empty folds
 
-foldr₁ : ∀ {n} → (A → A → A) → Vec A (suc n) → A
+foldr₁ : (A → A → A) → Vec A (suc n) → A
 foldr₁ _⊕_ (x ∷ [])     = x
 foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)
 
-foldl₁ : ∀ {n} → (A → A → A) → Vec A (suc n) → A
+foldl₁ : (A → A → A) → Vec A (suc n) → A
 foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs
 
 -- Special folds
 
-sum : ∀ {n} → Vec ℕ n → ℕ
+sum : Vec ℕ n → ℕ
 sum = foldr _ _+_ 0
 
-count : ∀ {P : Pred A p} → Decidable P → ∀ {n} → Vec A n → ℕ
+count : ∀ {P : Pred A p} → Decidable P → Vec A n → ℕ
 count P? []       = zero
 count P? (x ∷ xs) with does (P? x)
 ... | true  = suc (count P? xs)
@@ -238,11 +233,11 @@ count P? (x ∷ xs) with does (P? x)
 [_] : A → Vec A 1
 [ x ] = x ∷ []
 
-replicate : ∀ {n} → A → Vec A n
+replicate : A → Vec A n
 replicate {n = zero}  x = []
 replicate {n = suc n} x = x ∷ replicate x
 
-tabulate : ∀ {n} → (Fin n → A) → Vec A n
+tabulate : (Fin n → A) → Vec A n
 tabulate {n = zero}  f = []
 tabulate {n = suc n} f = f zero ∷ tabulate (f ∘ suc)
 
@@ -275,18 +270,18 @@ group (suc n) k .(ys ++ zs)         | (ys , zs , refl) with group n k zs
 group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) =
   ((ys ∷ zss) , refl)
 
-split : ∀ {n} → Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
+split : Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
 split []           = ([]     , [])
 split (x ∷ [])     = (x ∷ [] , [])
 split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs)
 
-uncons : ∀ {n} → Vec A (suc n) → A × Vec A n
+uncons : Vec A (suc n) → A × Vec A n
 uncons (x ∷ xs) = x , xs
 
 ------------------------------------------------------------------------
 -- Operations for converting between lists
 
-toList : ∀ {n} → Vec A n → List A
+toList : Vec A n → List A
 toList []       = List.[]
 toList (x ∷ xs) = List._∷_ x (toList xs)
 
@@ -301,42 +296,40 @@ fromList (List._∷_ x xs) = x ∷ fromList xs
 
 infixl 5 _∷ʳ_
 
-_∷ʳ_ : ∀ {n} → Vec A n → A → Vec A (suc n)
+_∷ʳ_ : Vec A n → A → Vec A (suc n)
 []       ∷ʳ y = [ y ]
 (x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)
 
 -- vanilla reverse
 
-reverse : ∀ {n} → Vec A n → Vec A n
-reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
+reverse : Vec A n → Vec A n
+reverse = foldl (Vec _) (λ rev x → x ∷ rev) []
 
 -- reverse-append
 
 infix 5 _ʳ++_
 
-_ʳ++_ : ∀ {m n} → Vec A m → Vec A n → Vec A (m + n)
-_ʳ++_ {A = A} {n = n} xs ys = foldl ((Vec A) ∘ (_+ n)) (λ rev x → x ∷ rev) ys xs
+_ʳ++_ : Vec A m → Vec A n → Vec A (m + n)
+xs ʳ++ ys = foldl (Vec _ ∘ (_+ _)) (λ rev x → x ∷ rev) ys xs
 
 -- init and last
 
-initLast : ∀ {n} (xs : Vec A (1 + n)) →
-           ∃₂ λ (ys : Vec A n) (y : A) → xs ≡ ys ∷ʳ y
-initLast {n = zero}  (x ∷ [])         = ([] , x , refl)
-initLast {n = suc n} (x ∷ xs)         with initLast xs
-initLast {n = suc n} (x ∷ .(ys ∷ʳ y)) | (ys , y , refl) =
-  ((x ∷ ys) , y , refl)
+initLast : ∀ (xs : Vec A (1 + n)) → ∃₂ λ ys y → xs ≡ ys ∷ʳ y
+initLast {n = zero}  (x ∷ []) = ([] , x , refl)
+initLast {n = suc n} (x ∷ xs) with initLast xs
+... | (ys , y , refl) = (x ∷ ys , y , refl)
 
-init : ∀ {n} → Vec A (1 + n) → Vec A n
-init xs         with initLast xs
-init .(ys ∷ʳ y) | (ys , y , refl) = ys
+init : Vec A (1 + n) → Vec A n
+init xs with initLast xs
+... | (ys , y , refl) = ys
 
-last : ∀ {n} → Vec A (1 + n) → A
-last xs         with initLast xs
-last .(ys ∷ʳ y) | (ys , y , refl) = y
+last : Vec A (1 + n) → A
+last xs with initLast xs
+... | (ys , y , refl) = y
 
 ------------------------------------------------------------------------
 -- Other operations
 
-transpose : ∀ {m n} → Vec (Vec A n) m → Vec (Vec A m) n
+transpose : Vec (Vec A n) m → Vec (Vec A m) n
 transpose []         = replicate []
 transpose (as ∷ ass) = replicate _∷_ ⊛ as ⊛ transpose ass
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index d3d7d9887a..e6d83aef35 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -10,7 +10,6 @@ module Data.Vec.Properties where
 
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
-open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base
@@ -23,48 +22,46 @@ open import Data.Vec.Base
 open import Function.Base
 open import Function.Inverse using (_↔_; inverse)
 open import Level using (Level)
-open import Relation.Binary as B hiding (Decidable)
-open import Relation.Binary.PropositionalEquality as P
-  using (_≡_; _≢_; refl; _≗_; cong₂)
-open P.≡-Reasoning
+open import Relation.Binary hiding (Decidable)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary using (Dec; does; yes; no)
 open import Relation.Nullary.Decidable using (map′)
 open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Negation using (contradiction)
+
+open ≡-Reasoning
 
 private
   variable
     a b c d p : Level
-    A : Set a
-    B : Set b
-    C : Set c
-    D : Set d
+    A B C D : Set a
+    w x y z : A
+    m n : ℕ
+    ws xs ys zs : Vec A n
 
 ------------------------------------------------------------------------
 -- Properties of propositional equality over vectors
 
-module _ {n} {x y : A} {xs ys : Vec A n} where
-
- ∷-injectiveˡ : x ∷ xs ≡ y ∷ ys → x ≡ y
- ∷-injectiveˡ refl = refl
+∷-injectiveˡ : x ∷ xs ≡ y ∷ ys → x ≡ y
+∷-injectiveˡ refl = refl
 
- ∷-injectiveʳ : x ∷ xs ≡ y ∷ ys → xs ≡ ys
- ∷-injectiveʳ refl = refl
+∷-injectiveʳ : x ∷ xs ≡ y ∷ ys → xs ≡ ys
+∷-injectiveʳ refl = refl
 
- ∷-injective : (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
- ∷-injective refl = refl , refl
+∷-injective : (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys
+∷-injective refl = refl , refl
 
-≡-dec : B.Decidable _≡_ → ∀ {n} → B.Decidable {A = Vec A n} _≡_
+≡-dec : DecidableEquality A → DecidableEquality (Vec A n)
 ≡-dec _≟_ []       []       = yes refl
-≡-dec _≟_ (x ∷ xs) (y ∷ ys) =
-  map′ (uncurry (cong₂ _∷_)) ∷-injective
-       (x ≟ y ×-dec ≡-dec _≟_ xs ys)
+≡-dec _≟_ (x ∷ xs) (y ∷ ys) = map′ (uncurry (cong₂ _∷_))
+  ∷-injective (x ≟ y ×-dec ≡-dec _≟_ xs ys)
 
 ------------------------------------------------------------------------
 -- _[_]=_
 
-[]=-injective : ∀ {n} {xs : Vec A n} {i x y} →
-                xs [ i ]= x → xs [ i ]= y → x ≡ y
+[]=-injective : ∀ {i} → xs [ i ]= x → xs [ i ]= y → x ≡ y
 []=-injective here          here          = refl
 []=-injective (there xsᵢ≡x) (there xsᵢ≡y) = []=-injective xsᵢ≡x xsᵢ≡y
 
@@ -73,49 +70,49 @@ module _ {n} {x y : A} {xs ys : Vec A n} where
 ------------------------------------------------------------------------
 -- take
 
-unfold-take : ∀ n {m} x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
+unfold-take : ∀ n x (xs : Vec A (n + m)) → take (suc n) (x ∷ xs) ≡ x ∷ take n xs
 unfold-take n x xs with splitAt n xs
-unfold-take n x .(xs ++ ys) | xs , ys , refl = refl
+... | xs , ys , refl = refl
 
-take-distr-zipWith : ∀ {m n} → (f : A → B → C) →
-                     (xs : Vec A (m + n)) → (ys : Vec B (m + n)) →
+take-distr-zipWith : ∀ (f : A → B → C) →
+                     (xs : Vec A (m + n)) (ys : Vec B (m + n)) →
                      take m (zipWith f xs ys) ≡ zipWith f (take m xs) (take m ys)
-take-distr-zipWith {m = zero}  f  xs       ys = refl
+take-distr-zipWith {m = zero}  f xs       ys       = refl
 take-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin
     take (suc m) (zipWith f (x ∷ xs) (y ∷ ys))
   ≡⟨⟩
     take (suc m) (f x y ∷ (zipWith f xs ys))
   ≡⟨ unfold-take m (f x y) (zipWith f xs ys) ⟩
     f x y ∷ take m (zipWith f xs ys)
-  ≡⟨ P.cong (f x y ∷_) (take-distr-zipWith f xs ys) ⟩
+  ≡⟨ cong (f x y ∷_) (take-distr-zipWith f xs ys) ⟩
     f x y ∷ (zipWith f (take m xs) (take m ys))
   ≡⟨⟩
     zipWith f (x ∷ (take m xs)) (y ∷ (take m ys))
-  ≡˘⟨ P.cong₂ (zipWith f) (unfold-take m x xs) (unfold-take m y ys) ⟩
+  ≡˘⟨ cong₂ (zipWith f) (unfold-take m x xs) (unfold-take m y ys) ⟩
     zipWith f (take (suc m) (x ∷ xs)) (take (suc m) (y ∷ ys))
   ∎
 
-take-distr-map : ∀ {n} → (f : A → B) → (m : ℕ) → (xs : Vec A (m + n)) →
+take-distr-map : ∀ (f : A → B) (m : ℕ) (xs : Vec A (m + n)) →
                  take m (map f xs) ≡ map f (take m xs)
 take-distr-map f zero xs = refl
-take-distr-map f (suc m) (x ∷ xs) =
-  begin
-    take (suc m) (map f (x ∷ xs)) ≡⟨⟩
-    take (suc m) (f x ∷ map f xs) ≡⟨ unfold-take m (f x) (map f xs) ⟩
-    f x ∷ (take m (map f xs))     ≡⟨ P.cong (f x ∷_) (take-distr-map f m xs) ⟩
-    f x ∷ (map f (take m xs))     ≡⟨⟩
-    map f (x ∷ take m xs)         ≡˘⟨ P.cong (map f) (unfold-take m x xs) ⟩
-    map f (take (suc m) (x ∷ xs)) ∎
+take-distr-map f (suc m) (x ∷ xs) = begin
+  take (suc m) (map f (x ∷ xs)) ≡⟨⟩
+  take (suc m) (f x ∷ map f xs) ≡⟨ unfold-take m (f x) (map f xs) ⟩
+  f x ∷ (take m (map f xs))     ≡⟨ cong (f x ∷_) (take-distr-map f m xs) ⟩
+  f x ∷ (map f (take m xs))     ≡⟨⟩
+  map f (x ∷ take m xs)         ≡˘⟨ cong (map f) (unfold-take m x xs) ⟩
+  map f (take (suc m) (x ∷ xs)) ∎
 
 ------------------------------------------------------------------------
 -- drop
 
-unfold-drop : ∀ n {m} x (xs : Vec A (n + m)) → drop (suc n) (x ∷ xs) ≡ drop n xs
+unfold-drop : ∀ n x (xs : Vec A (n + m)) →
+              drop (suc n) (x ∷ xs) ≡ drop n xs
 unfold-drop n x xs with splitAt n xs
-unfold-drop n x .(xs ++ ys) | xs , ys , refl = refl
+... | xs , ys , refl = refl
 
-drop-distr-zipWith : ∀ {m n} → (f : A → B → C) →
-                     (x : Vec A (m + n)) → (y : Vec B (m + n)) →
+drop-distr-zipWith : (f : A → B → C) →
+                     (x : Vec A (m + n)) (y : Vec B (m + n)) →
                      drop m (zipWith f x y) ≡ zipWith f (drop m x) (drop m y)
 drop-distr-zipWith {m = zero} f   xs       ys = refl
 drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin
@@ -126,24 +123,24 @@ drop-distr-zipWith {m = suc m} f (x ∷ xs) (y ∷ ys) = begin
     drop m (zipWith f xs ys)
   ≡⟨ drop-distr-zipWith f xs ys ⟩
     zipWith f (drop m xs) (drop m ys)
-  ≡˘⟨ P.cong₂ (zipWith f) (unfold-drop m x xs) (unfold-drop m y ys) ⟩
+  ≡˘⟨ cong₂ (zipWith f) (unfold-drop m x xs) (unfold-drop m y ys) ⟩
     zipWith f (drop (suc m) (x ∷ xs)) (drop (suc m) (y ∷ ys))
   ∎
 
-drop-distr-map : ∀ {n} → (f : A → B) → (m : ℕ) → (x : Vec A (m + n)) →
+drop-distr-map : ∀ (f : A → B) (m : ℕ) (x : Vec A (m + n)) →
                  drop m (map f x) ≡ map f (drop m x)
 drop-distr-map f zero x = refl
 drop-distr-map f (suc m) (x ∷ xs) = begin
   drop (suc m) (map f (x ∷ xs)) ≡⟨⟩
-  drop (suc m) (f x ∷ map f xs) ≡⟨ unfold-drop m (f x) (map f xs) ⟩
-  drop m (map f xs)             ≡⟨ drop-distr-map f m xs ⟩
-  map f (drop m xs)             ≡⟨ P.cong (map f) (P.sym (unfold-drop m x xs)) ⟩
+  drop (suc m) (f x ∷ map f xs) ≡⟨  unfold-drop m (f x) (map f xs) ⟩
+  drop m (map f xs)             ≡⟨  drop-distr-map f m xs ⟩
+  map f (drop m xs)             ≡˘⟨ cong (map f) (unfold-drop m x xs) ⟩
   map f (drop (suc m) (x ∷ xs)) ∎
 
 ------------------------------------------------------------------------
 -- take and drop together
 
-take-drop-id : ∀ {n} → (m : ℕ) → (x : Vec A (m + n)) → take m x ++ drop m x ≡ x
+take-drop-id : ∀ (m : ℕ) (x : Vec A (m + n)) → take m x ++ drop m x ≡ x
 take-drop-id zero x = refl
 take-drop-id (suc m) (x ∷ xs) = begin
     take (suc m) (x ∷ xs) ++ drop (suc m) (x ∷ xs)
@@ -151,71 +148,64 @@ take-drop-id (suc m) (x ∷ xs) = begin
     (x ∷ take m xs) ++ (drop m xs)
   ≡⟨⟩
     x ∷ (take m xs ++ drop m xs)
-  ≡⟨ P.cong (x ∷_) (take-drop-id m xs) ⟩
+  ≡⟨ cong (x ∷_) (take-drop-id m xs) ⟩
     x ∷ xs
   ∎
 
 ------------------------------------------------------------------------
 -- lookup
 
-[]=⇒lookup : ∀ {n} {x : A} {xs} {i : Fin n} →
-             xs [ i ]= x → lookup xs i ≡ x
+[]=⇒lookup : ∀ {i} → xs [ i ]= x → lookup xs i ≡ x
 []=⇒lookup here            = refl
 []=⇒lookup (there xs[i]=x) = []=⇒lookup xs[i]=x
 
-lookup⇒[]= : ∀ {n} (i : Fin n) {x : A} xs →
-             lookup xs i ≡ x → xs [ i ]= x
+lookup⇒[]= : ∀ (i : Fin n) xs → lookup xs i ≡ x → xs [ i ]= x
 lookup⇒[]= zero    (_ ∷ _)  refl = here
 lookup⇒[]= (suc i) (_ ∷ xs) p    = there (lookup⇒[]= i xs p)
 
-[]=↔lookup : ∀ {n i} {x} {xs : Vec A n} →
-             xs [ i ]= x ↔ lookup xs i ≡ x
+[]=↔lookup : ∀ {i} → xs [ i ]= x ↔ lookup xs i ≡ x
 []=↔lookup {i = i} =
   inverse []=⇒lookup (lookup⇒[]= _ _)
           lookup⇒[]=∘[]=⇒lookup ([]=⇒lookup∘lookup⇒[]= _ i)
   where
-  lookup⇒[]=∘[]=⇒lookup :
-    ∀ {n x xs} {i : Fin n} (p : xs [ i ]= x) →
-    lookup⇒[]= i xs ([]=⇒lookup p) ≡ p
+  lookup⇒[]=∘[]=⇒lookup : ∀ {i} (p : xs [ i ]= x) →
+                          lookup⇒[]= i xs ([]=⇒lookup p) ≡ p
   lookup⇒[]=∘[]=⇒lookup here      = refl
-  lookup⇒[]=∘[]=⇒lookup (there p) =
-    P.cong there (lookup⇒[]=∘[]=⇒lookup p)
+  lookup⇒[]=∘[]=⇒lookup (there p) = cong there (lookup⇒[]=∘[]=⇒lookup p)
 
-  []=⇒lookup∘lookup⇒[]= :
-    ∀ {n} xs (i : Fin n) {x} (p : lookup xs i ≡ x) →
-    []=⇒lookup (lookup⇒[]= i xs p) ≡ p
+  []=⇒lookup∘lookup⇒[]= : ∀ xs (i : Fin n) (p : lookup xs i ≡ x) →
+                          []=⇒lookup (lookup⇒[]= i xs p) ≡ p
   []=⇒lookup∘lookup⇒[]= (x ∷ xs) zero    refl = refl
-  []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p    =
-    []=⇒lookup∘lookup⇒[]= xs i p
+  []=⇒lookup∘lookup⇒[]= (x ∷ xs) (suc i) p    = []=⇒lookup∘lookup⇒[]= xs i p
 
-lookup-inject≤-take : ∀ m {n} (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
+lookup-inject≤-take : ∀ m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) →
                       lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i
 lookup-inject≤-take (suc m) m≤m+n zero (x ∷ xs)
   rewrite unfold-take m x xs = refl
-lookup-inject≤-take (suc (suc m)) m≤m+n (suc zero) (x ∷ x' ∷ xs)
-  rewrite unfold-take (suc m) x (x' ∷ xs) | unfold-take m x' xs = refl
-lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷ x' ∷ xs)
-  rewrite unfold-take (suc m) x (x' ∷ xs) | unfold-take m x' xs = lookup-inject≤-take m m≤m+n i xs
+lookup-inject≤-take (suc (suc m)) m≤m+n (suc zero) (x ∷ y ∷ xs)
+  rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = refl
+lookup-inject≤-take (suc (suc m)) (s≤s (s≤s m≤m+n)) (suc (suc i)) (x ∷ y ∷ xs)
+  rewrite unfold-take (suc m) x (y ∷ xs) | unfold-take m y xs = lookup-inject≤-take m m≤m+n i xs
 
 ------------------------------------------------------------------------
 -- updateAt (_[_]%=_)
 
 -- (+) updateAt i actually updates the element at index i.
 
-updateAt-updates : ∀ {n} (i : Fin n) {f : A → A} (xs : Vec A n) {x : A} →
+updateAt-updates : ∀ (i : Fin n) {f : A → A} (xs : Vec A n) →
                    xs [ i ]= x → (updateAt i f xs) [ i ]= f x
 updateAt-updates zero    (x ∷ xs) here        = here
 updateAt-updates (suc i) (x ∷ xs) (there loc) = there (updateAt-updates i xs loc)
 
 -- (-) updateAt i does not touch the elements at other indices.
 
-updateAt-minimal : ∀ {n} (i j : Fin n) {f : A → A} {x : A} (xs : Vec A n) →
+updateAt-minimal : ∀ (i j : Fin n) {f : A → A} (xs : Vec A n) →
                    i ≢ j → xs [ i ]= x → (updateAt j f xs) [ i ]= x
-updateAt-minimal zero    zero    (x ∷ xs) 0≢0 here        = ⊥-elim (0≢0 refl)
+updateAt-minimal zero    zero    (x ∷ xs) 0≢0 here        = contradiction refl 0≢0
 updateAt-minimal zero    (suc j) (x ∷ xs) _   here        = here
 updateAt-minimal (suc i) zero    (x ∷ xs) _   (there loc) = there loc
 updateAt-minimal (suc i) (suc j) (x ∷ xs) i≢j (there loc) =
-  there (updateAt-minimal i j xs (i≢j ∘ P.cong suc) loc)
+  there (updateAt-minimal i j xs (i≢j ∘ cong suc) loc)
 
 -- The other properties are consequences of (+) and (-).
 -- We spell the most natural properties out.
@@ -231,31 +221,30 @@ updateAt-minimal (suc i) (suc j) (x ∷ xs) i≢j (there loc) =
 -- 1a. relative identity:  f = id ↾ (lookup xs i)
 --                implies  updateAt i f = id ↾ xs
 
-updateAt-id-relative : ∀ {n} (i : Fin n) {f : A → A} (xs : Vec A n) →
+updateAt-id-relative : ∀ (i : Fin n) {f : A → A} (xs : Vec A n) →
                        f (lookup xs i) ≡ lookup xs i →
                        updateAt i f xs ≡ xs
-updateAt-id-relative zero    (x ∷ xs) eq = P.cong (_∷ xs) eq
-updateAt-id-relative (suc i) (x ∷ xs) eq = P.cong (x ∷_) (updateAt-id-relative i xs eq)
+updateAt-id-relative zero    (x ∷ xs) eq = cong (_∷ xs) eq
+updateAt-id-relative (suc i) (x ∷ xs) eq = cong (x ∷_) (updateAt-id-relative i xs eq)
 
 -- 1b. identity:  updateAt i id ≗ id
 
-updateAt-id : ∀ {n} (i : Fin n) (xs : Vec A n) →
-              updateAt i id xs ≡ xs
+updateAt-id : ∀ (i : Fin n) (xs : Vec A n) → updateAt i id xs ≡ xs
 updateAt-id i xs = updateAt-id-relative i xs refl
 
 -- 2a. relative composition:  f ∘ g = h ↾ (lookup xs i)
 --                   implies  updateAt i f ∘ updateAt i g = updateAt i h ↾ xs
 
-updateAt-compose-relative : ∀ {n} (i : Fin n) {f g h : A → A} (xs : Vec A n) →
+updateAt-compose-relative : ∀ (i : Fin n) {f g h : A → A} (xs : Vec A n) →
                             f (g (lookup xs i)) ≡ h (lookup xs i) →
                             updateAt i f (updateAt i g xs) ≡ updateAt i h xs
-updateAt-compose-relative zero    (x ∷ xs) fg=h = P.cong (_∷ xs) fg=h
+updateAt-compose-relative zero    (x ∷ xs) fg=h = cong (_∷ xs) fg=h
 updateAt-compose-relative (suc i) (x ∷ xs) fg=h =
-  P.cong (x ∷_) (updateAt-compose-relative i xs fg=h)
+  cong (x ∷_) (updateAt-compose-relative i xs fg=h)
 
 -- 2b. composition:  updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
 
-updateAt-compose : ∀ {n} (i : Fin n) {f g : A → A} →
+updateAt-compose : ∀ (i : Fin n) {f g : A → A} →
                    updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
 updateAt-compose i xs = updateAt-compose-relative i xs refl
 
@@ -264,15 +253,15 @@ updateAt-compose i xs = updateAt-compose-relative i xs refl
 -- 3a.  If    f = g ↾ (lookup xs i)
 --      then  updateAt i f = updateAt i g ↾ xs
 
-updateAt-cong-relative : ∀ {n} (i : Fin n) {f g : A → A} (xs : Vec A n) →
+updateAt-cong-relative : ∀ (i : Fin n) {f g : A → A} (xs : Vec A n) →
                          f (lookup xs i) ≡ g (lookup xs i) →
                          updateAt i f xs ≡ updateAt i g xs
-updateAt-cong-relative zero    (x ∷ xs) f=g = P.cong (_∷ xs) f=g
-updateAt-cong-relative (suc i) (x ∷ xs) f=g = P.cong (x ∷_) (updateAt-cong-relative i xs f=g)
+updateAt-cong-relative zero    (x ∷ xs) f=g = cong (_∷ xs) f=g
+updateAt-cong-relative (suc i) (x ∷ xs) f=g = cong (x ∷_) (updateAt-cong-relative i xs f=g)
 
 -- 3b. congruence:  f ≗ g → updateAt i f ≗ updateAt i g
 
-updateAt-cong : ∀ {n} (i : Fin n) {f g : A → A} →
+updateAt-cong : ∀ (i : Fin n) {f g : A → A} →
                 f ≗ g → updateAt i f ≗ updateAt i g
 updateAt-cong i f≗g xs = updateAt-cong-relative i xs (f≗g (lookup xs i))
 
@@ -281,288 +270,285 @@ updateAt-cong i f≗g xs = updateAt-cong-relative i xs (f≗g (lookup xs i))
 -- This a consequence of updateAt-updates and updateAt-minimal
 -- but easier to prove inductively.
 
-updateAt-commutes : ∀ {n} (i j : Fin n) {f g : A → A} → i ≢ j →
+updateAt-commutes : ∀ (i j : Fin n) {f g : A → A} → i ≢ j →
                     updateAt i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f
-updateAt-commutes zero    zero    0≢0 (x ∷ xs) = ⊥-elim (0≢0 refl)
+updateAt-commutes zero    zero    0≢0 (x ∷ xs) = contradiction refl 0≢0
 updateAt-commutes zero    (suc j) i≢j (x ∷ xs) = refl
 updateAt-commutes (suc i) zero    i≢j (x ∷ xs) = refl
 updateAt-commutes (suc i) (suc j) i≢j (x ∷ xs) =
-  P.cong (x ∷_) (updateAt-commutes i j (i≢j ∘ P.cong suc) xs)
+  cong (x ∷_) (updateAt-commutes i j (i≢j ∘ cong suc) xs)
 
 -- lookup after updateAt reduces.
 
 -- For same index this is an easy consequence of updateAt-updates
 -- using []=↔lookup.
 
-lookup∘updateAt : ∀ {n} (i : Fin n) {f : A → A} →
-                  ∀ xs → lookup (updateAt i f xs) i ≡ f (lookup xs i)
+lookup∘updateAt : ∀ (i : Fin n) {f : A → A} xs →
+                  lookup (updateAt i f xs) i ≡ f (lookup xs i)
 lookup∘updateAt i xs =
   []=⇒lookup (updateAt-updates i xs (lookup⇒[]= i _ refl))
 
 -- For different indices it easily follows from updateAt-minimal.
 
-lookup∘updateAt′ : ∀ {n} (i j : Fin n) {f : A → A} → i ≢ j →
-                   ∀ xs → lookup (updateAt j f xs) i ≡ lookup xs i
+lookup∘updateAt′ : ∀ (i j : Fin n) {f : A → A} → i ≢ j → ∀ xs →
+                   lookup (updateAt j f xs) i ≡ lookup xs i
 lookup∘updateAt′ i j xs i≢j =
   []=⇒lookup (updateAt-minimal i j i≢j xs (lookup⇒[]= i _ refl))
 
 -- Aliases for notation _[_]%=_
 
-[]%=-id : ∀ {n} (xs : Vec A n) (i : Fin n) → xs [ i ]%= id ≡ xs
+[]%=-id : ∀ (xs : Vec A n) (i : Fin n) → xs [ i ]%= id ≡ xs
 []%=-id xs i = updateAt-id i xs
 
-[]%=-compose : ∀ {n} (xs : Vec A n) (i : Fin n) {f g : A → A} →
+[]%=-compose : ∀ (xs : Vec A n) (i : Fin n) {f g : A → A} →
      xs [ i ]%= f
         [ i ]%= g
    ≡ xs [ i ]%= g ∘ f
 []%=-compose xs i = updateAt-compose i xs
 
+
 ------------------------------------------------------------------------
 -- _[_]≔_ (update)
 --
 -- _[_]≔_ is defined in terms of updateAt, and all of its properties
 -- are special cases of the ones for updateAt.
 
-[]≔-idempotent : ∀ {n} (xs : Vec A n) (i : Fin n) {x₁ x₂ : A} →
-                 (xs [ i ]≔ x₁) [ i ]≔ x₂ ≡ xs [ i ]≔ x₂
+[]≔-idempotent : ∀ (xs : Vec A n) (i : Fin n) →
+                 (xs [ i ]≔ x) [ i ]≔ y ≡ xs [ i ]≔ y
 []≔-idempotent xs i = updateAt-compose i xs
 
-[]≔-commutes : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j →
+[]≔-commutes : ∀ (xs : Vec A n) (i j : Fin n) → i ≢ j →
                (xs [ i ]≔ x) [ j ]≔ y ≡ (xs [ j ]≔ y) [ i ]≔ x
-[]≔-commutes xs i j i≢j = updateAt-commutes j i (i≢j ∘ P.sym) xs
+[]≔-commutes xs i j i≢j = updateAt-commutes j i (i≢j ∘ sym) xs
 
-[]≔-updates : ∀ {n} (xs : Vec A n) (i : Fin n) {x : A} →
-              (xs [ i ]≔ x) [ i ]= x
+[]≔-updates : ∀ (xs : Vec A n) (i : Fin n) → (xs [ i ]≔ x) [ i ]= x
 []≔-updates xs i = updateAt-updates i xs (lookup⇒[]= i xs refl)
 
-[]≔-minimal : ∀ {n} (xs : Vec A n) (i j : Fin n) {x y : A} → i ≢ j →
+[]≔-minimal : ∀ (xs : Vec A n) (i j : Fin n) → i ≢ j →
               xs [ i ]= x → (xs [ j ]≔ y) [ i ]= x
 []≔-minimal xs i j i≢j loc = updateAt-minimal i j xs i≢j loc
 
-[]≔-lookup : ∀ {n} (xs : Vec A n) (i : Fin n) →
-             xs [ i ]≔ lookup xs i ≡ xs
+[]≔-lookup : ∀ (xs : Vec A n) (i : Fin n) → xs [ i ]≔ lookup xs i ≡ xs
 []≔-lookup xs i = updateAt-id-relative i xs refl
 
-[]≔-++-↑ˡ : ∀ {m n x} (xs : Vec A m) (ys : Vec A n) i →
-                 (xs ++ ys) [ i ↑ˡ n ]≔ x ≡ (xs [ i ]≔ x) ++ ys
+[]≔-++-↑ˡ : ∀ (xs : Vec A m) (ys : Vec A n) i →
+            (xs ++ ys) [ i ↑ˡ n ]≔ x ≡ (xs [ i ]≔ x) ++ ys
 []≔-++-↑ˡ (x ∷ xs) ys zero    = refl
 []≔-++-↑ˡ (x ∷ xs) ys (suc i) =
-  P.cong (x ∷_) $ []≔-++-↑ˡ xs ys i
+  cong (x ∷_) $ []≔-++-↑ˡ xs ys i
 
-[]≔-++-↑ʳ : ∀ {m n y} (xs : Vec A m) (ys : Vec A n) i →
-                 (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y)
+[]≔-++-↑ʳ : ∀ (xs : Vec A m) (ys : Vec A n) i →
+            (xs ++ ys) [ m ↑ʳ i ]≔ y ≡ xs ++ (ys [ i ]≔ y)
 []≔-++-↑ʳ {m = zero}     []    (y ∷ ys) i = refl
-[]≔-++-↑ʳ {m = suc n} (x ∷ xs) (y ∷ ys) i = P.cong (x ∷_) $ []≔-++-↑ʳ xs (y ∷ ys) i
+[]≔-++-↑ʳ {m = suc n} (x ∷ xs) (y ∷ ys) i = cong (x ∷_) $ []≔-++-↑ʳ xs (y ∷ ys) i
 
-lookup∘update : ∀ {n} (i : Fin n) (xs : Vec A n) x →
+lookup∘update : ∀ (i : Fin n) (xs : Vec A n) x →
                 lookup (xs [ i ]≔ x) i ≡ x
 lookup∘update i xs x = lookup∘updateAt i xs
 
-lookup∘update′ : ∀ {n} {i j : Fin n} → i ≢ j → ∀ (xs : Vec A n) y →
+lookup∘update′ : ∀ {i j} → i ≢ j → ∀ (xs : Vec A n) y →
                  lookup (xs [ j ]≔ y) i ≡ lookup xs i
 lookup∘update′ {i = i} {j} i≢j xs y = lookup∘updateAt′ i j i≢j xs
 
 ------------------------------------------------------------------------
 -- map
 
-map-id : ∀ {n} → map {A = A} {n = n} id ≗ id
+map-id : map id ≗ id {A = Vec A n}
 map-id []       = refl
-map-id (x ∷ xs) = P.cong (x ∷_) (map-id xs)
+map-id (x ∷ xs) = cong (x ∷_) (map-id xs)
 
-map-const : ∀ {n} (xs : Vec A n) (y : B) → map (const y) xs ≡ replicate y
-map-const [] _ = refl
-map-const (_ ∷ xs) y = P.cong (y ∷_) (map-const xs y)
+map-const : ∀ (xs : Vec A n) (y : B) → map (const y) xs ≡ replicate y
+map-const []       _ = refl
+map-const (_ ∷ xs) y = cong (y ∷_) (map-const xs y)
 
-map-++ : ∀ {m} {n} (f : A → B) (xs : Vec A m) (ys : Vec A n) →
+map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) →
          map f (xs ++ ys) ≡ map f xs ++ map f ys
 map-++ f []       ys = refl
-map-++ f (x ∷ xs) ys = P.cong (f x ∷_) (map-++ f xs ys)
+map-++ f (x ∷ xs) ys = cong (f x ∷_) (map-++ f xs ys)
 
-map-cong : ∀ {n} {f g : A → B} → f ≗ g → map {n = n} f ≗ map g
+map-cong : ∀ {f g : A → B} → f ≗ g → map {n = n} f ≗ map g
 map-cong f≗g []       = refl
-map-cong f≗g (x ∷ xs) = P.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
+map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs)
 
-map-∘ : ∀ {n} (f : B → C) (g : A → B) →
+map-∘ : ∀ (f : B → C) (g : A → B) →
         map {n = n} (f ∘ g) ≗ map f ∘ map g
 map-∘ f g []       = refl
-map-∘ f g (x ∷ xs) = P.cong (f (g x) ∷_) (map-∘ f g xs)
+map-∘ f g (x ∷ xs) = cong (f (g x) ∷_) (map-∘ f g xs)
 
-lookup-map : ∀ {n} (i : Fin n) (f : A → B) (xs : Vec A n) →
+lookup-map : ∀ (i : Fin n) (f : A → B) (xs : Vec A n) →
              lookup (map f xs) i ≡ f (lookup xs i)
 lookup-map zero    f (x ∷ xs) = refl
 lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs
 
-map-updateAt : ∀ {n} {f : A → B} {g : A → A} {h : B → B}
+map-updateAt : ∀ {f : A → B} {g : A → A} {h : B → B}
                (xs : Vec A n) (i : Fin n) →
                f (g (lookup xs i)) ≡ h (f (lookup xs i)) →
                map f (updateAt i g xs) ≡ updateAt i h (map f xs)
-map-updateAt (x ∷ xs) zero    eq = P.cong (_∷ _) eq
-map-updateAt (x ∷ xs) (suc i) eq = P.cong (_ ∷_) (map-updateAt xs i eq)
+map-updateAt (x ∷ xs) zero    eq = cong (_∷ _) eq
+map-updateAt (x ∷ xs) (suc i) eq = cong (_ ∷_) (map-updateAt xs i eq)
 
-map-[]≔ : ∀ {n} (f : A → B) (xs : Vec A n) (i : Fin n) {x : A} →
+map-[]≔ : ∀ (f : A → B) (xs : Vec A n) (i : Fin n) →
           map f (xs [ i ]≔ x) ≡ map f xs [ i ]≔ f x
 map-[]≔ f xs i = map-updateAt xs i refl
 
-map-⊛ : ∀ {n} (f : A → B → C) (g : A → B) (xs : Vec A n) →
+map-⊛ : ∀ (f : A → B → C) (g : A → B) (xs : Vec A n) →
         (map f xs ⊛ map g xs) ≡ map (f ˢ g) xs
-map-⊛ f g [] = refl
-map-⊛ f g (x ∷ xs) = P.cong (f x (g x) ∷_) (map-⊛ f g xs)
+map-⊛ f g []       = refl
+map-⊛ f g (x ∷ xs) = cong (f x (g x) ∷_) (map-⊛ f g xs)
 
 ------------------------------------------------------------------------
 -- _++_
 
-module _ {m} {ys ys′ : Vec A m} where
+-- See also Data.Vec.Properties.WithK.++-assoc.
 
-  -- See also Data.Vec.Properties.WithK.++-assoc.
+++-injectiveˡ : ∀ {n} (ws xs : Vec A n) → ws ++ ys ≡ xs ++ zs → ws ≡ xs
+++-injectiveˡ []       []         _  = refl
+++-injectiveˡ (_ ∷ ws) (_ ∷ xs) eq =
+  cong₂ _∷_ (∷-injectiveˡ eq) (++-injectiveˡ _ _ (∷-injectiveʳ eq))
 
-  ++-injectiveˡ : ∀ {n} (xs xs′ : Vec A n) →
-                  xs ++ ys ≡ xs′ ++ ys′ → xs ≡ xs′
-  ++-injectiveˡ []       []         _  = refl
-  ++-injectiveˡ (x ∷ xs) (x′ ∷ xs′) eq =
-    P.cong₂ _∷_ (∷-injectiveˡ eq) (++-injectiveˡ _ _ (∷-injectiveʳ eq))
+++-injectiveʳ : ∀ {n} (ws xs : Vec A n) → ws ++ ys ≡ xs ++ zs → ys ≡ zs
+++-injectiveʳ []       []         eq = eq
+++-injectiveʳ (x ∷ ws) (x′ ∷ xs) eq =
+  ++-injectiveʳ ws xs (∷-injectiveʳ eq)
 
-  ++-injectiveʳ : ∀ {n} (xs xs′ : Vec A n) →
-                  xs ++ ys ≡ xs′ ++ ys′ → ys ≡ ys′
-  ++-injectiveʳ []       []         eq = eq
-  ++-injectiveʳ (x ∷ xs) (x′ ∷ xs′) eq =
-    ++-injectiveʳ xs xs′ (∷-injectiveʳ eq)
+++-injective  : ∀ (ws xs : Vec A n) →
+                ws ++ ys ≡ xs ++ zs → ws ≡ xs × ys ≡ zs
+++-injective ws xs eq =
+  (++-injectiveˡ ws xs eq , ++-injectiveʳ ws xs eq)
 
-  ++-injective  : ∀ {n} (xs xs′ : Vec A n) →
-                  xs ++ ys ≡ xs′ ++ ys′ → xs ≡ xs′ × ys ≡ ys′
-  ++-injective xs xs′ eq =
-    (++-injectiveˡ xs xs′ eq , ++-injectiveʳ xs xs′ eq)
-
-lookup-++-< : ∀ {m n} (xs : Vec A m) (ys : Vec A n) →
+lookup-++-< : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i<m : toℕ i < m) →
               lookup (xs ++ ys) i  ≡ lookup xs (Fin.fromℕ< i<m)
 lookup-++-< (x ∷ xs) ys zero    (s≤s z≤n)       = refl
 lookup-++-< (x ∷ xs) ys (suc i) (s≤s (s≤s i<m)) =
   lookup-++-< xs ys i (s≤s i<m)
 
-lookup-++-≥ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) →
+lookup-++-≥ : ∀ (xs : Vec A m) (ys : Vec A n) →
               ∀ i (i≥m : toℕ i ≥ m) →
               lookup (xs ++ ys) i ≡ lookup ys (Fin.reduce≥ i i≥m)
 lookup-++-≥ []       ys i       i≥m       = refl
 lookup-++-≥ (x ∷ xs) ys (suc i) (s≤s i≥m) = lookup-++-≥ xs ys i i≥m
 
-lookup-++ˡ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) i →
+lookup-++ˡ : ∀ (xs : Vec A m) (ys : Vec A n) i →
              lookup (xs ++ ys) (i ↑ˡ n) ≡ lookup xs i
 lookup-++ˡ (x ∷ xs) ys zero    = refl
 lookup-++ˡ (x ∷ xs) ys (suc i) = lookup-++ˡ xs ys i
 
-lookup-++ʳ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) i →
+lookup-++ʳ : ∀ (xs : Vec A m) (ys : Vec A n) i →
              lookup (xs ++ ys) (m ↑ʳ i) ≡ lookup ys i
 lookup-++ʳ []       ys       zero    = refl
 lookup-++ʳ []       (y ∷ xs) (suc i) = lookup-++ʳ [] xs i
 lookup-++ʳ (x ∷ xs) ys       i       = lookup-++ʳ xs ys i
 
-lookup-splitAt : ∀ m {n} (xs : Vec A m) (ys : Vec A n) i →
+lookup-splitAt : ∀ m (xs : Vec A m) (ys : Vec A n) i →
                 lookup (xs ++ ys) i ≡ [ lookup xs , lookup ys ]′
                 (Fin.splitAt m i)
 lookup-splitAt zero    []       ys i       = refl
 lookup-splitAt (suc m) (x ∷ xs) ys zero    = refl
-lookup-splitAt (suc m) (x ∷ xs) ys (suc i) = P.trans
+lookup-splitAt (suc m) (x ∷ xs) ys (suc i) = trans
   (lookup-splitAt m xs ys i)
-  (P.sym ([,]-map-commute (Fin.splitAt m i)))
+  (sym ([,]-map-commute (Fin.splitAt m i)))
 
 ------------------------------------------------------------------------
 -- zipWith
 
 module _ {f : A → A → A} where
 
-  zipWith-assoc : Associative _≡_ f → ∀ {n} →
+  zipWith-assoc : Associative _≡_ f →
                   Associative _≡_ (zipWith {n = n} f)
   zipWith-assoc assoc []       []       []       = refl
   zipWith-assoc assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) =
-    P.cong₂ _∷_ (assoc x y z) (zipWith-assoc assoc xs ys zs)
+    cong₂ _∷_ (assoc x y z) (zipWith-assoc assoc xs ys zs)
 
-  zipWith-idem : Idempotent _≡_ f → ∀ {n} →
+  zipWith-idem : Idempotent _≡_ f →
                  Idempotent _≡_ (zipWith {n = n} f)
   zipWith-idem idem []       = refl
   zipWith-idem idem (x ∷ xs) =
-    P.cong₂ _∷_ (idem x) (zipWith-idem idem xs)
+    cong₂ _∷_ (idem x) (zipWith-idem idem xs)
 
 module _ {f : A → A → A} {e : A} where
 
-  zipWith-identityˡ : LeftIdentity _≡_ e f → ∀ {n} →
+  zipWith-identityˡ : LeftIdentity _≡_ e f →
                       LeftIdentity _≡_ (replicate e) (zipWith {n = n} f)
   zipWith-identityˡ idˡ []       = refl
   zipWith-identityˡ idˡ (x ∷ xs) =
-    P.cong₂ _∷_ (idˡ x) (zipWith-identityˡ idˡ xs)
+    cong₂ _∷_ (idˡ x) (zipWith-identityˡ idˡ xs)
 
-  zipWith-identityʳ : RightIdentity _≡_ e f → ∀ {n} →
+  zipWith-identityʳ : RightIdentity _≡_ e f →
                       RightIdentity _≡_ (replicate e) (zipWith {n = n} f)
   zipWith-identityʳ idʳ []       = refl
   zipWith-identityʳ idʳ (x ∷ xs) =
-    P.cong₂ _∷_ (idʳ x) (zipWith-identityʳ idʳ xs)
+    cong₂ _∷_ (idʳ x) (zipWith-identityʳ idʳ xs)
 
-  zipWith-zeroˡ : LeftZero _≡_ e f → ∀ {n} →
+  zipWith-zeroˡ : LeftZero _≡_ e f →
                   LeftZero _≡_ (replicate e) (zipWith {n = n} f)
   zipWith-zeroˡ zeˡ []       = refl
   zipWith-zeroˡ zeˡ (x ∷ xs) =
-    P.cong₂ _∷_ (zeˡ x) (zipWith-zeroˡ zeˡ xs)
+    cong₂ _∷_ (zeˡ x) (zipWith-zeroˡ zeˡ xs)
 
-  zipWith-zeroʳ : RightZero _≡_ e f → ∀ {n} →
+  zipWith-zeroʳ : RightZero _≡_ e f →
                   RightZero _≡_ (replicate e) (zipWith {n = n} f)
   zipWith-zeroʳ zeʳ []       = refl
   zipWith-zeroʳ zeʳ (x ∷ xs) =
-    P.cong₂ _∷_ (zeʳ x) (zipWith-zeroʳ zeʳ xs)
+    cong₂ _∷_ (zeʳ x) (zipWith-zeroʳ zeʳ xs)
+
+module _ {f : A → A → A} {e : A} {⁻¹ : A → A} where
 
-  zipWith-inverseˡ : ∀ {⁻¹} → LeftInverse _≡_ e ⁻¹ f → ∀ {n} →
+  zipWith-inverseˡ : LeftInverse _≡_ e ⁻¹ f →
                      LeftInverse _≡_ (replicate {n = n} e) (map ⁻¹) (zipWith f)
   zipWith-inverseˡ invˡ []       = refl
   zipWith-inverseˡ invˡ (x ∷ xs) =
-    P.cong₂ _∷_ (invˡ x) (zipWith-inverseˡ invˡ xs)
+    cong₂ _∷_ (invˡ x) (zipWith-inverseˡ invˡ xs)
 
-  zipWith-inverseʳ : ∀ {⁻¹} → RightInverse _≡_ e ⁻¹ f → ∀ {n} →
+  zipWith-inverseʳ : RightInverse _≡_ e ⁻¹ f →
                      RightInverse _≡_ (replicate {n = n} e) (map ⁻¹) (zipWith f)
   zipWith-inverseʳ invʳ []       = refl
   zipWith-inverseʳ invʳ (x ∷ xs) =
-    P.cong₂ _∷_ (invʳ x) (zipWith-inverseʳ invʳ xs)
+    cong₂ _∷_ (invʳ x) (zipWith-inverseʳ invʳ xs)
 
 module _ {f g : A → A → A} where
 
-  zipWith-distribˡ : _DistributesOverˡ_ _≡_ f g → ∀ {n} →
+  zipWith-distribˡ : _DistributesOverˡ_ _≡_ f g →
                      _DistributesOverˡ_ _≡_ (zipWith {n = n} f) (zipWith g)
   zipWith-distribˡ distribˡ []        []      []       = refl
   zipWith-distribˡ distribˡ (x ∷ xs) (y ∷ ys) (z ∷ zs) =
-    P.cong₂ _∷_ (distribˡ x y z) (zipWith-distribˡ distribˡ xs ys zs)
+    cong₂ _∷_ (distribˡ x y z) (zipWith-distribˡ distribˡ xs ys zs)
 
-  zipWith-distribʳ : _DistributesOverʳ_ _≡_ f g → ∀ {n} →
+  zipWith-distribʳ : _DistributesOverʳ_ _≡_ f g →
                      _DistributesOverʳ_ _≡_ (zipWith {n = n} f) (zipWith g)
   zipWith-distribʳ distribʳ []        []      []       = refl
   zipWith-distribʳ distribʳ (x ∷ xs) (y ∷ ys) (z ∷ zs) =
-    P.cong₂ _∷_ (distribʳ x y z) (zipWith-distribʳ distribʳ xs ys zs)
+    cong₂ _∷_ (distribʳ x y z) (zipWith-distribʳ distribʳ xs ys zs)
 
-  zipWith-absorbs : _Absorbs_ _≡_ f g → ∀ {n} →
+  zipWith-absorbs : _Absorbs_ _≡_ f g →
                    _Absorbs_ _≡_ (zipWith {n = n} f) (zipWith g)
   zipWith-absorbs abs []       []       = refl
   zipWith-absorbs abs (x ∷ xs) (y ∷ ys) =
-    P.cong₂ _∷_ (abs x y) (zipWith-absorbs abs xs ys)
+    cong₂ _∷_ (abs x y) (zipWith-absorbs abs xs ys)
 
-module _ {f : A → A → B} where
+module _ {f : A → B → C} {g : B → A → C} where
 
-  zipWith-comm : (∀ x y → f x y ≡ f y x) → ∀ {n}
-                 (xs ys : Vec A n) → zipWith f xs ys ≡ zipWith f ys xs
+  zipWith-comm : ∀ (comm : ∀ x y → f x y ≡ g y x) (xs : Vec A n) ys →
+                 zipWith f xs ys ≡ zipWith g ys xs
   zipWith-comm comm []       []       = refl
   zipWith-comm comm (x ∷ xs) (y ∷ ys) =
-    P.cong₂ _∷_ (comm x y) (zipWith-comm comm xs ys)
+    cong₂ _∷_ (comm x y) (zipWith-comm comm xs ys)
 
-zipWith-map₁ : ∀ {n} (_⊕_ : B → C → D) (f : A → B)
+zipWith-map₁ : ∀ (_⊕_ : B → C → D) (f : A → B)
                (xs : Vec A n) (ys : Vec C n) →
                zipWith _⊕_ (map f xs) ys ≡ zipWith (λ x y → f x ⊕ y) xs ys
 zipWith-map₁ _⊕_ f []       []       = refl
 zipWith-map₁ _⊕_ f (x ∷ xs) (y ∷ ys) =
-  P.cong (f x ⊕ y ∷_) (zipWith-map₁ _⊕_ f xs ys)
+  cong (f x ⊕ y ∷_) (zipWith-map₁ _⊕_ f xs ys)
 
-zipWith-map₂ : ∀ {n} (_⊕_ : A → C → D) (f : B → C)
+zipWith-map₂ : ∀ (_⊕_ : A → C → D) (f : B → C)
                (xs : Vec A n) (ys : Vec B n) →
                zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys
 zipWith-map₂ _⊕_ f []       []       = refl
 zipWith-map₂ _⊕_ f (x ∷ xs) (y ∷ ys) =
-  P.cong (x ⊕ f y ∷_) (zipWith-map₂ _⊕_ f xs ys)
+  cong (x ⊕ f y ∷_) (zipWith-map₂ _⊕_ f xs ys)
 
-lookup-zipWith : ∀ (f : A → B → C) {n} (i : Fin n) xs ys →
+lookup-zipWith : ∀ (f : A → B → C) (i : Fin n) xs ys →
                  lookup (zipWith f xs ys) i ≡ f (lookup xs i) (lookup ys i)
 lookup-zipWith _ zero    (x ∷ _)  (y ∷ _)   = refl
 lookup-zipWith _ (suc i) (_ ∷ xs) (_ ∷ ys)  = lookup-zipWith _ i xs ys
@@ -570,99 +556,97 @@ lookup-zipWith _ (suc i) (_ ∷ xs) (_ ∷ ys)  = lookup-zipWith _ i xs ys
 ------------------------------------------------------------------------
 -- zip
 
-lookup-zip : ∀ {n} (i : Fin n) (xs : Vec A n) (ys : Vec B n) →
+lookup-zip : ∀ (i : Fin n) (xs : Vec A n) (ys : Vec B n) →
              lookup (zip xs ys) i ≡ (lookup xs i , lookup ys i)
 lookup-zip = lookup-zipWith _,_
 
 -- map lifts projections to vectors of products.
 
-map-proj₁-zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
+map-proj₁-zip : ∀ (xs : Vec A n) (ys : Vec B n) →
                 map proj₁ (zip xs ys) ≡ xs
 map-proj₁-zip []       []       = refl
-map-proj₁-zip (x ∷ xs) (y ∷ ys) = P.cong (x ∷_) (map-proj₁-zip xs ys)
+map-proj₁-zip (x ∷ xs) (y ∷ ys) = cong (x ∷_) (map-proj₁-zip xs ys)
 
-map-proj₂-zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
+map-proj₂-zip : ∀ (xs : Vec A n) (ys : Vec B n) →
                 map proj₂ (zip xs ys) ≡ ys
 map-proj₂-zip []       []       = refl
-map-proj₂-zip (x ∷ xs) (y ∷ ys) = P.cong (y ∷_) (map-proj₂-zip xs ys)
+map-proj₂-zip (x ∷ xs) (y ∷ ys) = cong (y ∷_) (map-proj₂-zip xs ys)
 
 -- map lifts pairing to vectors of products.
 
-map-<,>-zip : ∀ {n} (f : A → B) (g : A → C) (xs : Vec A n) →
+map-<,>-zip : ∀ (f : A → B) (g : A → C) (xs : Vec A n) →
               map < f , g > xs ≡ zip (map f xs) (map g xs)
-map-<,>-zip f g []       = P.refl
-map-<,>-zip f g (x ∷ xs) = P.cong (_ ∷_) (map-<,>-zip f g xs)
+map-<,>-zip f g []       = refl
+map-<,>-zip f g (x ∷ xs) = cong (_ ∷_) (map-<,>-zip f g xs)
 
-map-zip : ∀ {n} (f : A → B) (g : C → D) (xs : Vec A n) (ys : Vec C n) →
+map-zip : ∀ (f : A → B) (g : C → D) (xs : Vec A n) (ys : Vec C n) →
           map (Prod.map f g) (zip xs ys) ≡ zip (map f xs) (map g ys)
 map-zip f g []       []       = refl
-map-zip f g (x ∷ xs) (y ∷ ys) = P.cong (_ ∷_) (map-zip f g xs ys)
+map-zip f g (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (map-zip f g xs ys)
 
 ------------------------------------------------------------------------
 -- unzip
 
-lookup-unzip : ∀ {n} (i : Fin n) (xys : Vec (A × B) n) →
+lookup-unzip : ∀ (i : Fin n) (xys : Vec (A × B) n) →
                let xs , ys = unzip xys
                in (lookup xs i , lookup ys i) ≡ lookup xys i
 lookup-unzip ()      []
 lookup-unzip zero    ((x , y) ∷ xys) = refl
 lookup-unzip (suc i) ((x , y) ∷ xys) = lookup-unzip i xys
 
-map-unzip : ∀ {n} (f : A → B) (g : C → D) (xys : Vec (A × C) n) →
+map-unzip : ∀ (f : A → B) (g : C → D) (xys : Vec (A × C) n) →
             let xs , ys = unzip xys
             in (map f xs , map g ys) ≡ unzip (map (Prod.map f g) xys)
 map-unzip f g []              = refl
 map-unzip f g ((x , y) ∷ xys) =
-  P.cong (Prod.map (f x ∷_) (g y ∷_)) (map-unzip f g xys)
+  cong (Prod.map (f x ∷_) (g y ∷_)) (map-unzip f g xys)
 
 -- Products of vectors are isomorphic to vectors of products.
 
-unzip∘zip : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
+unzip∘zip : ∀ (xs : Vec A n) (ys : Vec B n) →
             unzip (zip xs ys) ≡ (xs , ys)
 unzip∘zip [] []             = refl
 unzip∘zip (x ∷ xs) (y ∷ ys) =
-  P.cong (Prod.map (x ∷_) (y ∷_)) (unzip∘zip xs ys)
+  cong (Prod.map (x ∷_) (y ∷_)) (unzip∘zip xs ys)
 
-zip∘unzip : ∀ {n} (xys : Vec (A × B) n) →
-            uncurry zip (unzip xys) ≡ xys
-zip∘unzip []              = refl
-zip∘unzip ((x , y) ∷ xys) = P.cong ((x , y) ∷_) (zip∘unzip xys)
+zip∘unzip : ∀ (xys : Vec (A × B) n) → uncurry zip (unzip xys) ≡ xys
+zip∘unzip []         = refl
+zip∘unzip (xy ∷ xys) = cong (xy ∷_) (zip∘unzip xys)
 
-×v↔v× : ∀ {n} → (Vec A n × Vec B n) ↔ Vec (A × B) n
+×v↔v× : (Vec A n × Vec B n) ↔ Vec (A × B) n
 ×v↔v× = inverse (uncurry zip) unzip (uncurry unzip∘zip) zip∘unzip
 
 ------------------------------------------------------------------------
 -- _⊛_
 
-lookup-⊛ : ∀ {n} i (fs : Vec (A → B) n) (xs : Vec A n) →
+lookup-⊛ : ∀ i (fs : Vec (A → B) n) (xs : Vec A n) →
            lookup (fs ⊛ xs) i ≡ (lookup fs i $ lookup xs i)
 lookup-⊛ zero    (f ∷ fs) (x ∷ xs) = refl
 lookup-⊛ (suc i) (f ∷ fs) (x ∷ xs) = lookup-⊛ i fs xs
 
-map-is-⊛ : ∀ {n} (f : A → B) (xs : Vec A n) →
+map-is-⊛ : ∀ (f : A → B) (xs : Vec A n) →
            map f xs ≡ (replicate f ⊛ xs)
 map-is-⊛ f []       = refl
-map-is-⊛ f (x ∷ xs) = P.cong (_ ∷_) (map-is-⊛ f xs)
+map-is-⊛ f (x ∷ xs) = cong (_ ∷_) (map-is-⊛ f xs)
 
-⊛-is-zipWith : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) →
+⊛-is-zipWith : ∀ (fs : Vec (A → B) n) (xs : Vec A n) →
                (fs ⊛ xs) ≡ zipWith _$_ fs xs
 ⊛-is-zipWith []       []       = refl
-⊛-is-zipWith (f ∷ fs) (x ∷ xs) = P.cong (f x ∷_) (⊛-is-zipWith fs xs)
+⊛-is-zipWith (f ∷ fs) (x ∷ xs) = cong (f x ∷_) (⊛-is-zipWith fs xs)
 
-zipWith-is-⊛ : ∀ {n} (f : A → B → C) (xs : Vec A n) (ys : Vec B n) →
+zipWith-is-⊛ : ∀ (f : A → B → C) (xs : Vec A n) (ys : Vec B n) →
                zipWith f xs ys ≡ (replicate f ⊛ xs ⊛ ys)
 zipWith-is-⊛ f []       []       = refl
-zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = P.cong (_ ∷_) (zipWith-is-⊛ f xs ys)
+zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (zipWith-is-⊛ f xs ys)
 
-⊛-is->>= : ∀ {n} (fs : Vec (A → B) n) (xs : Vec A n) →
+⊛-is->>= : ∀ (fs : Vec (A → B) n) (xs : Vec A n) →
            (fs ⊛ xs) ≡ (fs DiagonalBind.>>= flip map xs)
-⊛-is->>= [] [] = refl
-⊛-is->>= (f ∷ fs) (x ∷ xs) = P.cong (f x ∷_) $ begin
+⊛-is->>= []       []       = refl
+⊛-is->>= (f ∷ fs) (x ∷ xs) = cong (f x ∷_) $ begin
   fs ⊛ xs                                          ≡⟨ ⊛-is->>= fs xs ⟩
   diagonal (map (flip map xs) fs)                  ≡⟨⟩
-  diagonal (map (tail ∘ flip map (x ∷ xs)) fs)     ≡⟨ P.cong diagonal (map-∘ _ _ _) ⟩
+  diagonal (map (tail ∘ flip map (x ∷ xs)) fs)     ≡⟨ cong diagonal (map-∘ _ _ _) ⟩
   diagonal (map tail (map (flip map (x ∷ xs)) fs)) ∎
-  where open P.≡-Reasoning
 
 ------------------------------------------------------------------------
 -- foldl
@@ -675,14 +659,13 @@ foldl-universal : ∀ (B : ℕ → Set b) (f : FoldlOp A B) e
                   (∀ {c} {C} {g : FoldlOp A C} e → h {c} C g e [] ≡ e) →
                   (∀ {c} {C} {g : FoldlOp A C} e {n} x →
                    (h {c} C g e {suc n}) ∘ (x ∷_) ≗ h (C ∘ suc) g (g e x)) →
-                  ∀ {n} → h B f e ≗ foldl B {n} f e
+                  h B f e ≗ foldl {n = n} B f e
 foldl-universal B f e h base step []       = base e
 foldl-universal B f e h base step (x ∷ xs) = begin
   h B f e (x ∷ xs)             ≡⟨ step e x xs ⟩
   h (B ∘ suc) f (f e x) xs     ≡⟨ foldl-universal _ f (f e x) h base step xs ⟩
   foldl (B ∘ suc) f (f e x) xs ≡⟨⟩
   foldl B f e (x ∷ xs)         ∎
-  where open P.≡-Reasoning
 
 foldl-fusion : ∀ {B : ℕ → Set b} {C : ℕ → Set c}
                (h : ∀ {n} → B n → C n) →
@@ -690,58 +673,19 @@ foldl-fusion : ∀ {B : ℕ → Set b} {C : ℕ → Set c}
                {g : FoldlOp A C} {e : C zero} →
                (h d ≡ e) →
                (∀ {n} b x → h (f {n} b x) ≡ g (h b) x) →
-               ∀ {n} → h ∘ foldl B {n} f d ≗ foldl C g e
+               h ∘ foldl {n = n} B f d ≗ foldl C g e
 foldl-fusion h {f} {d} {g} {e} base fuse []       = base
 foldl-fusion h {f} {d} {g} {e} base fuse (x ∷ xs) =
   foldl-fusion h eq fuse xs
   where
-    open P.≡-Reasoning
     eq : h (f d x) ≡ g e x
     eq = begin
-       h (f d x) ≡⟨ fuse d x ⟩
-       g (h d) x ≡⟨ P.cong (λ e → g e x) base ⟩
-       g e x     ∎
-
-------------------------------------------------------------------------
--- _∷ʳ_, _ʳ++_ and reverse
-
--- reverse of cons is snoc of reverse.
-
-reverse-∷ : ∀ {n} x (xs : Vec A n) → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
-reverse-∷ x xs = P.sym (foldl-fusion (_∷ʳ x) refl (λ b x → refl) xs)
-
--- reverse-append is append of reverse.
-
-unfold-ʳ++ : ∀ {m n} (xs : Vec A m) (ys : Vec A n) → xs ʳ++ ys ≡ reverse xs ++ ys
-unfold-ʳ++ xs ys = P.sym (foldl-fusion (_++ ys) refl (λ b x → refl) xs)
-
-------------------------------------------------------------------------
--- misc. properties of foldl
-
--- foldl and _-∷ʳ_
-
-foldl-∷ʳ : ∀ (B : ℕ → Set b) (f : FoldlOp A B) {n} e y (ys : Vec A n) →
-           foldl B f e (ys ∷ʳ y) ≡ f (foldl B f e ys) y
-foldl-∷ʳ B f e y []       = refl
-foldl-∷ʳ B f e y (x ∷ xs) = foldl-∷ʳ (B ∘ suc) f (f e x) y xs
-
-module _ (B : ℕ → Set b) (f : FoldlOp A B) {e : B zero} where
-
-  foldl-[] : foldl B f e [] ≡ e
-  foldl-[] = refl
-
-  -- foldl after a reverse is a foldr
-
-  foldl-reverse : ∀ {n} → foldl B {n} f e ∘ reverse ≗ foldr B (flip f) e
-  foldl-reverse []       = refl
-  foldl-reverse (x ∷ xs) = begin
-    foldl B f e (reverse (x ∷ xs)) ≡⟨ P.cong (foldl B f e) (reverse-∷ x xs) ⟩
-    foldl B f e (reverse xs ∷ʳ x)  ≡⟨ foldl-∷ʳ B f e x (reverse xs) ⟩
-    f (foldl B f e (reverse xs)) x ≡⟨ P.cong (flip f x) (foldl-reverse xs) ⟩
-    f (foldr B (flip f) e xs) x    ≡⟨⟩
-    foldr B (flip f) e (x ∷ xs)    ∎
-    where open P.≡-Reasoning
+      h (f d x) ≡⟨ fuse d x ⟩
+      g (h d) x ≡⟨ cong (λ e → g e x) base ⟩
+      g e x     ∎
 
+foldl-[] : ∀ (B : ℕ → Set b) (f : FoldlOp A B) {e} → foldl B f e [] ≡ e
+foldl-[] _ _ = refl
 
 ------------------------------------------------------------------------
 -- foldr
@@ -755,253 +699,257 @@ module _ (B : ℕ → Set b) (f : FoldrOp A B) {e : B zero} where
   foldr-universal : (h : ∀ {n} → Vec A n → B n) →
                     h [] ≡ e →
                     (∀ {n} x → h ∘ (x ∷_) ≗ f {n} x ∘ h) →
-                    ∀ {n} → h ≗ foldr B {n} f e
+                    h ≗ foldr {n = n} B f e
   foldr-universal h base step []       = base
   foldr-universal h base step (x ∷ xs) = begin
     h (x ∷ xs)           ≡⟨ step x xs ⟩
-    f x (h xs)           ≡⟨ P.cong (f x) (foldr-universal h base step xs) ⟩
+    f x (h xs)           ≡⟨ cong (f x) (foldr-universal h base step xs) ⟩
     f x (foldr B f e xs) ∎
-    where open P.≡-Reasoning
 
   foldr-[] : foldr B f e [] ≡ e
   foldr-[] = refl
 
-  foldr-++ : ∀ {m n} (xs : Vec A m) {ys : Vec A n} →
+  foldr-++ : ∀ (xs : Vec A m) →
              foldr B f e (xs ++ ys) ≡ foldr (B ∘ (_+ n)) f (foldr B f e ys) xs
   foldr-++ []       = refl
-  foldr-++ (x ∷ xs) = P.cong (f x) (foldr-++ xs)
-
-  -- foldr and _-∷ʳ_
-
-  foldr-∷ʳ : ∀ {n} y (ys : Vec A n) →
-             foldr B f e (ys ∷ʳ y) ≡ foldr (B ∘ suc) f (f y e) ys
-  foldr-∷ʳ y [] = refl
-  foldr-∷ʳ y (x ∷ xs) = P.cong (f x) (foldr-∷ʳ y xs)
-
-  -- foldr after a reverse-append is a foldl
-
-  foldr-ʳ++ : ∀ {m} {n} (xs : Vec A m) {ys : Vec A n} →
-              foldr B f e (xs ʳ++ ys) ≡
-              foldl (B ∘ (_+ n)) (flip f) (foldr B f e ys) xs
-  foldr-ʳ++ xs = foldl-fusion (foldr B f e) refl (λ _ _ → refl) xs
-
-  -- foldr after a reverse is a foldl
-
-  foldr-reverse : ∀ {n} → foldr B {n} f e ∘ reverse ≗ foldl B (flip f) e
-  foldr-reverse xs = foldl-fusion (foldr B f e) refl (λ _ _ → refl) xs
-
-
-------------------------------------------------------------------------
+  foldr-++ (x ∷ xs) = cong (f x) (foldr-++ xs)
 
 -- fusion and identity as consequences of universality
 
 foldr-fusion : ∀ {B : ℕ → Set b} {f : FoldrOp A B} e
-               {C : ℕ → Set c} {g : FoldrOp A C}
+                 {C : ℕ → Set c} {g : FoldrOp A C}
                (h : ∀ {n} → B n → C n) →
                (∀ {n} x → h ∘ f {n} x ≗ g x ∘ h) →
-               ∀ {n} → h ∘ foldr B {n} f e ≗ foldr C g (h e)
+               h ∘ foldr {n = n} B f e ≗ foldr C g (h e)
 foldr-fusion {B = B} {f} e {C} h fuse =
   foldr-universal C _ _ refl (λ x xs → fuse x (foldr B f e xs))
 
-id-is-foldr : ∀ {n} → id ≗ foldr (Vec A) {n} _∷_ []
+id-is-foldr : id ≗ foldr {n = n} (Vec A) _∷_ []
 id-is-foldr = foldr-universal _ _ id refl (λ _ _ → refl)
 
-++-is-foldr : ∀ {m n} (xs : Vec A m) {ys : Vec A n} →
+map-is-foldr : ∀ (f : A → B) →
+               map {n = n} f ≗ foldr (Vec B) (λ x ys → f x ∷ ys) []
+map-is-foldr f = foldr-universal (Vec _) (λ x ys → f x ∷ ys) (map f) refl (λ _ _ → refl)
+
+++-is-foldr : ∀ (xs : Vec A m) →
               xs ++ ys ≡ foldr (Vec A ∘ (_+ n)) _∷_ ys xs
-++-is-foldr {A = A} {n = n} xs {ys} =
+++-is-foldr {A = A} {n = n} {ys} xs =
   foldr-universal (Vec A ∘ (_+ n)) _∷_ (_++ ys) refl (λ _ _ → refl) xs
 
-
 ------------------------------------------------------------------------
 -- _∷ʳ_
 
-module _ {x y : A} where
+∷ʳ-injective : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
+∷ʳ-injective []       []        refl = (refl , refl)
+∷ʳ-injective (x ∷ xs) (y  ∷ ys) eq   with ∷-injective eq
+... | refl , eq′ = Prod.map₁ (cong (x ∷_)) (∷ʳ-injective xs ys eq′)
 
-  ∷ʳ-injective : ∀ {n} (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
-  ∷ʳ-injective []          []          refl = (refl , refl)
-  ∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with ∷-injective eq
-  ... | refl , eq′ = Prod.map₁ (P.cong (x ∷_)) (∷ʳ-injective xs ys eq′)
+∷ʳ-injectiveˡ : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
+∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq)
 
-  ∷ʳ-injectiveˡ : ∀ {n} (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
-  ∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq)
+∷ʳ-injectiveʳ : ∀ (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
+∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)
 
-  ∷ʳ-injectiveʳ : ∀ {n} (xs ys : Vec A n) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
-  ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)
+foldl-∷ʳ : ∀ (B : ℕ → Set b) (f : FoldlOp A B) e y (ys : Vec A n) →
+           foldl B f e (ys ∷ʳ y) ≡ f (foldl B f e ys) y
+foldl-∷ʳ B f e y []       = refl
+foldl-∷ʳ B f e y (x ∷ xs) = foldl-∷ʳ (B ∘ suc) f (f e x) y xs
 
+foldr-∷ʳ : ∀ (B : ℕ → Set b) (f : FoldrOp A B) {e} y (ys : Vec A n) →
+           foldr B f e (ys ∷ʳ y) ≡ foldr (B ∘ suc) f (f y e) ys
+foldr-∷ʳ B f y []       = refl
+foldr-∷ʳ B f y (x ∷ xs) = cong (f x) (foldr-∷ʳ B f y xs)
 
-------------------------------------------------------------------------
--- map and _∷ʳ_, _ʳ++_ and reverse
-
-module _ (f : A → B) where
-
-  map-is-foldr : ∀ {n} → map {n = n} f ≗ foldr (Vec B) (λ x ys → f x ∷ ys) []
-  map-is-foldr = foldr-universal (Vec B) (λ x ys → f x ∷ ys) (map f) refl (λ _ _ → refl)
-
-  -- map and _∷ʳ_
-
-  map-∷ʳ : ∀ {n} x (xs : Vec A n) →
-           map f (xs ∷ʳ x) ≡ (map f xs) ∷ʳ (f x)
-  map-∷ʳ x [] = refl
-  map-∷ʳ x (y ∷ xs) = P.cong (f y ∷_) (map-∷ʳ x xs)
-
-  -- map and reverse
-
-  map-reverse : ∀ {n} (xs : Vec A n) →
-                map f (reverse xs) ≡ reverse (map f xs)
-  map-reverse [] = refl
-  map-reverse (x ∷ xs) = begin
-    map f (reverse (x ∷ xs))  ≡⟨ P.cong (map f) (reverse-∷ x xs) ⟩
-    map f (reverse xs ∷ʳ x)   ≡⟨ map-∷ʳ x (reverse xs) ⟩
-    map f (reverse xs) ∷ʳ f x ≡⟨ P.cong (_∷ʳ f x) (map-reverse xs ) ⟩
-    reverse (map f xs) ∷ʳ f x ≡⟨ P.sym (reverse-∷ (f x) (map f xs)) ⟩
-    reverse (f x ∷ map f xs)  ≡⟨⟩
-    reverse (map f (x ∷ xs))  ∎
-    where open P.≡-Reasoning
-
-  -- map and _ʳ++_
-
-  map-ʳ++ : ∀ {m n} (xs : Vec A m) {ys : Vec A n} →
-            map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
-  map-ʳ++ xs {ys} = begin
-    map f (xs ʳ++ ys)              ≡⟨ P.cong (map f) (unfold-ʳ++ xs ys) ⟩
-    map f (reverse xs ++ ys)       ≡⟨ map-++ f (reverse xs) ys ⟩
-    map f (reverse xs) ++ map f ys ≡⟨ P.cong (_++ map f ys) (map-reverse xs) ⟩
-    reverse (map f xs) ++ map f ys ≡⟨ P.sym (unfold-ʳ++ (map f xs) (map f ys)) ⟩
-    map f xs ʳ++ map f ys          ∎
-    where open P.≡-Reasoning
+-- map and _∷ʳ_
+
+map-∷ʳ : ∀ (f : A → B) x (xs : Vec A n) → map f (xs ∷ʳ x) ≡ map f xs ∷ʳ f x
+map-∷ʳ f x []       = refl
+map-∷ʳ f x (y ∷ xs) = cong (f y ∷_) (map-∷ʳ f x xs)
 
 ------------------------------------------------------------------------
 -- reverse
 
+-- reverse of cons is snoc of reverse.
+
+reverse-∷ : ∀ x (xs : Vec A n) → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x
+reverse-∷ x xs = sym (foldl-fusion (_∷ʳ x) refl (λ b x → refl) xs)
+
+-- foldl after a reverse is a foldr
+
+foldl-reverse : ∀ (B : ℕ → Set b) (f : FoldlOp A B) {e} →
+                foldl {n = n} B f e ∘ reverse ≗ foldr B (flip f) e
+foldl-reverse _ _ {e} []       = refl
+foldl-reverse B f {e} (x ∷ xs) = begin
+  foldl B f e (reverse (x ∷ xs)) ≡⟨ cong (foldl B f e) (reverse-∷ x xs) ⟩
+  foldl B f e (reverse xs ∷ʳ x)  ≡⟨ foldl-∷ʳ B f e x (reverse xs) ⟩
+  f (foldl B f e (reverse xs)) x ≡⟨ cong (flip f x) (foldl-reverse B f xs) ⟩
+  f (foldr B (flip f) e xs) x    ≡⟨⟩
+  foldr B (flip f) e (x ∷ xs)    ∎
+
+-- foldr after a reverse is a foldl
+
+foldr-reverse : ∀ (B : ℕ → Set b) (f : FoldrOp A B) {e} →
+                foldr {n = n} B f e ∘ reverse ≗ foldl B (flip f) e
+foldr-reverse B f {e} xs = foldl-fusion (foldr B f e) refl (λ _ _ → refl) xs
+
 -- reverse is involutive.
 
-reverse-involutive : ∀ {n} → Involutive {A = Vec A n} _≡_ reverse
-reverse-involutive {A = A} xs = begin
-  reverse (reverse xs)    ≡⟨ foldl-reverse (Vec A) (λ b x → x ∷ b) xs ⟩
-  foldr (Vec A) _∷_ [] xs ≡⟨ P.sym (id-is-foldr xs) ⟩
+reverse-involutive : Involutive {A = Vec A n} _≡_ reverse
+reverse-involutive xs = begin
+  reverse (reverse xs)    ≡⟨  foldl-reverse (Vec _) (flip _∷_) xs ⟩
+  foldr (Vec _) _∷_ [] xs ≡˘⟨ id-is-foldr xs ⟩
   xs                      ∎
-  where open P.≡-Reasoning
 
-reverse-reverse : ∀ {n} {xs ys : Vec A n} →
-                  reverse xs ≡ ys → reverse ys ≡ xs
-reverse-reverse {xs = xs} {ys = ys} eq =  begin
-  reverse ys           ≡⟨ P.sym (P.cong reverse eq) ⟩
-  reverse (reverse xs) ≡⟨ reverse-involutive xs ⟩
+reverse-reverse : reverse xs ≡ ys → reverse ys ≡ xs
+reverse-reverse {xs = xs} {ys} eq =  begin
+  reverse ys           ≡˘⟨ cong reverse eq ⟩
+  reverse (reverse xs) ≡⟨  reverse-involutive xs ⟩
   xs                   ∎
-  where open P.≡-Reasoning
 
 -- reverse is injective.
 
-reverse-injective : ∀ {n} {xs ys : Vec A n} → reverse xs ≡ reverse ys → xs ≡ ys
-reverse-injective {n = n} {xs} {ys} eq = begin
-  xs                   ≡⟨ P.sym (reverse-reverse eq) ⟩
-  reverse (reverse ys) ≡⟨ reverse-involutive ys ⟩
+reverse-injective : reverse xs ≡ reverse ys → xs ≡ ys
+reverse-injective {xs = xs} {ys} eq = begin
+  xs                   ≡˘⟨ reverse-reverse eq ⟩
+  reverse (reverse ys) ≡⟨  reverse-involutive ys ⟩
   ys                   ∎
-  where open P.≡-Reasoning
 
+-- map and reverse
+
+map-reverse : ∀ (f : A → B) (xs : Vec A n) →
+              map f (reverse xs) ≡ reverse (map f xs)
+map-reverse f []       = refl
+map-reverse f (x ∷ xs) = begin
+  map f (reverse (x ∷ xs))  ≡⟨  cong (map f) (reverse-∷ x xs) ⟩
+  map f (reverse xs ∷ʳ x)   ≡⟨  map-∷ʳ f x (reverse xs) ⟩
+  map f (reverse xs) ∷ʳ f x ≡⟨  cong (_∷ʳ f x) (map-reverse f xs ) ⟩
+  reverse (map f xs) ∷ʳ f x ≡˘⟨ reverse-∷ (f x) (map f xs) ⟩
+  reverse (f x ∷ map f xs)  ≡⟨⟩
+  reverse (map f (x ∷ xs))  ∎
+
+------------------------------------------------------------------------
+-- _ʳ++_
+
+-- reverse-append is append of reverse.
+
+unfold-ʳ++ : ∀ (xs : Vec A m) (ys : Vec A n) → xs ʳ++ ys ≡ reverse xs ++ ys
+unfold-ʳ++ xs ys = sym (foldl-fusion (_++ ys) refl (λ b x → refl) xs)
+
+-- foldr after a reverse-append is a foldl
+
+foldr-ʳ++ : ∀ (B : ℕ → Set b) (f : FoldrOp A B) {e}
+            (xs : Vec A m) {ys : Vec A n} →
+            foldr B f e (xs ʳ++ ys) ≡
+            foldl (B ∘ (_+ n)) (flip f) (foldr B f e ys) xs
+foldr-ʳ++ B f {e} xs = foldl-fusion (foldr B f e) refl (λ _ _ → refl) xs
+
+-- map and _ʳ++_
+
+map-ʳ++ : ∀ (f : A → B) (xs : Vec A m) →
+          map f (xs ʳ++ ys) ≡ map f xs ʳ++ map f ys
+map-ʳ++ {ys = ys} f xs = begin
+  map f (xs ʳ++ ys)              ≡⟨  cong (map f) (unfold-ʳ++ xs ys) ⟩
+  map f (reverse xs ++ ys)       ≡⟨  map-++ f (reverse xs) ys ⟩
+  map f (reverse xs) ++ map f ys ≡⟨  cong (_++ map f ys) (map-reverse f xs) ⟩
+  reverse (map f xs) ++ map f ys ≡˘⟨ unfold-ʳ++ (map f xs) (map f ys) ⟩
+  map f xs ʳ++ map f ys          ∎
 
 ------------------------------------------------------------------------
 -- sum
 
-sum-++ : ∀ {m n} (xs : Vec ℕ m) {ys : Vec ℕ n} →
-         sum (xs ++ ys) ≡ sum xs + sum ys
-sum-++ []       {_}  = refl
-sum-++ (x ∷ xs) {ys} = begin
-  x + sum (xs ++ ys)     ≡⟨ P.cong (x +_) (sum-++ xs) ⟩
-  x + (sum xs + sum ys)  ≡⟨ P.sym (+-assoc x (sum xs) (sum ys)) ⟩
+sum-++ : ∀ (xs : Vec ℕ m) → sum (xs ++ ys) ≡ sum xs + sum ys
+sum-++ {_}       []       = refl
+sum-++ {ys = ys} (x ∷ xs) = begin
+  x + sum (xs ++ ys)     ≡⟨  cong (x +_) (sum-++ xs) ⟩
+  x + (sum xs + sum ys)  ≡˘⟨ +-assoc x (sum xs) (sum ys) ⟩
   sum (x ∷ xs) + sum ys  ∎
-  where open P.≡-Reasoning
-
 
 ------------------------------------------------------------------------
 -- replicate
 
-lookup-replicate : ∀ {n} (i : Fin n) (x : A) →
-                   lookup (replicate x) i ≡ x
-lookup-replicate zero    = λ _ → refl
-lookup-replicate (suc i) = lookup-replicate i
+lookup-replicate : ∀ (i : Fin n) (x : A) → lookup (replicate x) i ≡ x
+lookup-replicate zero    x = refl
+lookup-replicate (suc i) x = lookup-replicate i x
 
 map-replicate :  ∀ (f : A → B) (x : A) n →
                  map f (replicate x) ≡ replicate {n = n} (f x)
 map-replicate f x zero = refl
-map-replicate f x (suc n) = P.cong (f x ∷_) (map-replicate f x n)
+map-replicate f x (suc n) = cong (f x ∷_) (map-replicate f x n)
 
-transpose-replicate : ∀ {m n} (xs : Vec A m) → transpose (replicate {n = n} xs) ≡ map replicate xs
-transpose-replicate {n = zero} _ = P.sym (map-const _ [])
+transpose-replicate : ∀ (xs : Vec A m) →
+                      transpose (replicate {n = n} xs) ≡ map replicate xs
+transpose-replicate {n = zero}  _  = sym (map-const _ [])
 transpose-replicate {n = suc n} xs = begin
   transpose (replicate xs)                        ≡⟨⟩
-  (replicate _∷_ ⊛ xs ⊛ transpose (replicate xs)) ≡⟨ P.cong₂ _⊛_ (P.sym (map-is-⊛ _∷_ xs)) (transpose-replicate xs) ⟩
+  (replicate _∷_ ⊛ xs ⊛ transpose (replicate xs)) ≡⟨ cong₂ _⊛_ (sym (map-is-⊛ _∷_ xs)) (transpose-replicate xs) ⟩
   (map _∷_ xs ⊛ map replicate xs)                 ≡⟨ map-⊛ _∷_ replicate xs ⟩
   map replicate xs                                ∎
-  where open P.≡-Reasoning
 
-zipWith-replicate : ∀ {n : ℕ} (_⊕_ : A → B → C) (x : A) (y : B) →
+zipWith-replicate : ∀ (_⊕_ : A → B → C) (x : A) (y : B) →
                     zipWith {n = n} _⊕_ (replicate x) (replicate y) ≡ replicate (x ⊕ y)
 zipWith-replicate {n = zero}  _⊕_ x y = refl
-zipWith-replicate {n = suc n} _⊕_ x y = P.cong (x ⊕ y ∷_) (zipWith-replicate _⊕_ x y)
+zipWith-replicate {n = suc n} _⊕_ x y = cong (x ⊕ y ∷_) (zipWith-replicate _⊕_ x y)
 
-zipWith-replicate₁ : ∀ {n} (_⊕_ : A → B → C) (x : A) (ys : Vec B n) →
+zipWith-replicate₁ : ∀ (_⊕_ : A → B → C) (x : A) (ys : Vec B n) →
                      zipWith _⊕_ (replicate x) ys ≡ map (x ⊕_) ys
 zipWith-replicate₁ _⊕_ x []       = refl
 zipWith-replicate₁ _⊕_ x (y ∷ ys) =
-  P.cong (x ⊕ y ∷_) (zipWith-replicate₁ _⊕_ x ys)
+  cong (x ⊕ y ∷_) (zipWith-replicate₁ _⊕_ x ys)
 
-zipWith-replicate₂ : ∀ {n} (_⊕_ : A → B → C) (xs : Vec A n) (y : B) →
+zipWith-replicate₂ : ∀ (_⊕_ : A → B → C) (xs : Vec A n) (y : B) →
                      zipWith _⊕_ xs (replicate y) ≡ map (_⊕ y) xs
 zipWith-replicate₂ _⊕_ []       y = refl
 zipWith-replicate₂ _⊕_ (x ∷ xs) y =
-  P.cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y)
+  cong (x ⊕ y ∷_) (zipWith-replicate₂ _⊕_ xs y)
 
 ------------------------------------------------------------------------
 -- tabulate
 
-lookup∘tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) →
+lookup∘tabulate : ∀ (f : Fin n → A) (i : Fin n) →
                   lookup (tabulate f) i ≡ f i
 lookup∘tabulate f zero    = refl
 lookup∘tabulate f (suc i) = lookup∘tabulate (f ∘ suc) i
 
-tabulate∘lookup : ∀ {n} (xs : Vec A n) → tabulate (lookup xs) ≡ xs
+tabulate∘lookup : ∀ (xs : Vec A n) → tabulate (lookup xs) ≡ xs
 tabulate∘lookup []       = refl
-tabulate∘lookup (x ∷ xs) = P.cong (x ∷_) (tabulate∘lookup xs)
+tabulate∘lookup (x ∷ xs) = cong (x ∷_) (tabulate∘lookup xs)
 
-tabulate-∘ : ∀ {n} (f : A → B) (g : Fin n → A) →
+tabulate-∘ : ∀ (f : A → B) (g : Fin n → A) →
              tabulate (f ∘ g) ≡ map f (tabulate g)
 tabulate-∘ {n = zero}  f g = refl
-tabulate-∘ {n = suc n} f g = P.cong (f (g zero) ∷_) (tabulate-∘ f (g ∘ suc))
+tabulate-∘ {n = suc n} f g = cong (f (g zero) ∷_) (tabulate-∘ f (g ∘ suc))
 
-tabulate-cong : ∀ {n} {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
+tabulate-cong : ∀ {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g
 tabulate-cong {n = zero}  p = refl
-tabulate-cong {n = suc n} p = P.cong₂ _∷_ (p zero) (tabulate-cong (p ∘ suc))
+tabulate-cong {n = suc n} p = cong₂ _∷_ (p zero) (tabulate-cong (p ∘ suc))
 
 ------------------------------------------------------------------------
 -- allFin
 
-lookup-allFin : ∀ {n} (i : Fin n) → lookup (allFin n) i ≡ i
+lookup-allFin : ∀ (i : Fin n) → lookup (allFin n) i ≡ i
 lookup-allFin = lookup∘tabulate id
 
 allFin-map : ∀ n → allFin (suc n) ≡ zero ∷ map suc (allFin n)
-allFin-map n = P.cong (zero ∷_) $ tabulate-∘ suc id
+allFin-map n = cong (zero ∷_) $ tabulate-∘ suc id
 
-tabulate-allFin : ∀ {n} (f : Fin n → A) → tabulate f ≡ map f (allFin n)
+tabulate-allFin : ∀ (f : Fin n → A) → tabulate f ≡ map f (allFin n)
 tabulate-allFin f = tabulate-∘ f id
 
 -- If you look up every possible index, in increasing order, then you
 -- get back the vector you started with.
 
-map-lookup-allFin : ∀ {n} (xs : Vec A n) →
-                    map (lookup xs) (allFin n) ≡ xs
+map-lookup-allFin : ∀ (xs : Vec A n) → map (lookup xs) (allFin n) ≡ xs
 map-lookup-allFin {n = n} xs = begin
   map (lookup xs) (allFin n) ≡˘⟨ tabulate-∘ (lookup xs) id ⟩
   tabulate (lookup xs)       ≡⟨ tabulate∘lookup xs ⟩
   xs                         ∎
-  where open P.≡-Reasoning
 
 ------------------------------------------------------------------------
 -- count
 
 module _ {P : Pred A p} (P? : Decidable P) where
 
-  count≤n : ∀ {n} (xs : Vec A n) → count P? xs ≤ n
+  count≤n : ∀ (xs : Vec A n) → count P? xs ≤ n
   count≤n []       = z≤n
   count≤n (x ∷ xs) with does (P? x)
   ... | true  = s≤s (count≤n xs)
@@ -1010,49 +958,47 @@ module _ {P : Pred A p} (P? : Decidable P) where
 ------------------------------------------------------------------------
 -- insert
 
-insert-lookup : ∀ {n} (xs : Vec A n) (i : Fin (suc n)) (v : A) →
+insert-lookup : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
                 lookup (insert xs i v) i ≡ v
 insert-lookup xs       zero     v = refl
 insert-lookup (x ∷ xs) (suc i)  v = insert-lookup xs i v
 
-insert-punchIn : ∀ {n} (xs : Vec A n) (i : Fin (suc n)) (v : A)
-                 (j : Fin n) →
+insert-punchIn : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) (j : Fin n) →
                  lookup (insert xs i v) (Fin.punchIn i j) ≡ lookup xs j
 insert-punchIn xs       zero     v j       = refl
 insert-punchIn (x ∷ xs) (suc i)  v zero    = refl
 insert-punchIn (x ∷ xs) (suc i)  v (suc j) = insert-punchIn xs i v j
 
-remove-punchOut : ∀ {n} (xs : Vec A (suc n))
-                  {i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
+remove-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) →
                   lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j
-remove-punchOut (x ∷ xs) {zero} {zero} i≢j = ⊥-elim (i≢j refl)
-remove-punchOut (x ∷ xs) {zero} {suc j} i≢j = refl
-remove-punchOut (x ∷ y ∷ xs) {suc i} {zero} i≢j = refl
+remove-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction refl i≢j
+remove-punchOut (x ∷ xs)     {zero}  {suc j} i≢j = refl
+remove-punchOut (x ∷ y ∷ xs) {suc i} {zero}  i≢j = refl
 remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
-  remove-punchOut (y ∷ xs) (i≢j ∘ P.cong suc)
+  remove-punchOut (y ∷ xs) (i≢j ∘ cong suc)
 
 ------------------------------------------------------------------------
 -- remove
 
-remove-insert : ∀ {n} (xs : Vec A n) (i : Fin (suc n)) (v : A) →
+remove-insert : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
                 remove (insert xs i v) i ≡ xs
 remove-insert xs           zero           v = refl
 remove-insert (x ∷ xs)     (suc zero)     v = refl
 remove-insert (x ∷ y ∷ xs) (suc (suc i))  v =
-  P.cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v)
+  cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v)
 
-insert-remove : ∀ {n} (xs : Vec A (suc n)) (i : Fin (suc n)) →
+insert-remove : ∀ (xs : Vec A (suc n)) (i : Fin (suc n)) →
                 insert (remove xs i) i (lookup xs i) ≡ xs
 insert-remove (x ∷ xs)     zero     = refl
 insert-remove (x ∷ y ∷ xs) (suc i)  =
-  P.cong (x ∷_) (insert-remove (y ∷ xs) i)
+  cong (x ∷_) (insert-remove (y ∷ xs) i)
 
 ------------------------------------------------------------------------
 -- Conversion function
 
 toList∘fromList : (xs : List A) → toList (fromList xs) ≡ xs
 toList∘fromList List.[]       = refl
-toList∘fromList (x List.∷ xs) = P.cong (x List.∷_) (toList∘fromList xs)
+toList∘fromList (x List.∷ xs) = cong (x List.∷_) (toList∘fromList xs)
 
 
 ------------------------------------------------------------------------
@@ -1093,3 +1039,4 @@ sum-++-commute = sum-++
 "Warning: sum-++-commute was deprecated in v2.0.
 Please use sum-++ instead."
 #-}
+