diff --git a/README/Data/Tree/AVL.agda b/README/Data/Tree/AVL.agda
index abba7bfd0b..1b20d9a3b0 100644
--- a/README/Data/Tree/AVL.agda
+++ b/README/Data/Tree/AVL.agda
@@ -22,7 +22,7 @@ import Data.Tree.AVL
 open import Data.Nat.Properties using (<-strictTotalOrder)
 open import Data.Product as Prod using (_,_; _,′_)
 open import Data.String.Base using (String)
-open import Data.Vec using (Vec; _∷_; [])
+open import Data.Vec.Base using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
 
 open Data.Tree.AVL <-strictTotalOrder renaming (Tree to Tree′)
diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda
index a3e1de4a1b..5dc7c8951f 100644
--- a/src/Data/Nat/Binary/Subtraction.agda
+++ b/src/Data/Nat/Binary/Subtraction.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Binary.Properties
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Data.Vec using ([]; _∷_)
+open import Data.Vec.Base using ([]; _∷_)
 open import Function.Base using (_∘_; _$_)
 open import Level using (0ℓ)
 open import Relation.Binary
diff --git a/src/Data/Vec/Bounded.agda b/src/Data/Vec/Bounded.agda
index 3a1aae623e..35ecc6a96d 100644
--- a/src/Data/Vec/Bounded.agda
+++ b/src/Data/Vec/Bounded.agda
@@ -10,7 +10,8 @@ module Data.Vec.Bounded where
 
 open import Level using (Level)
 open import Data.Nat.Base
-open import Data.Vec as Vec using (Vec)
+open import Data.Vec.Base using (Vec)
+import Data.Vec as Vec using (filter; takeWhile; dropWhile)
 open import Function.Base using (id)
 open import Relation.Binary using (_Preserves_⟶_)
 open import Relation.Unary using (Pred; Decidable)
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
index 9c4486be47..e6cc006d89 100644
--- a/src/Data/Vec/Functional/Properties.agda
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -16,7 +16,7 @@ open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.List.Base as L using (List)
 import Data.List.Properties as Lₚ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
-open import Data.Vec as V using (Vec)
+open import Data.Vec.Base as V using (Vec)
 import Data.Vec.Properties as Vₚ
 open import Data.Vec.Functional
 open import Function.Base
diff --git a/src/Data/Vec/Membership/Propositional/Properties.agda b/src/Data/Vec/Membership/Propositional/Properties.agda
index 983e70ae63..f4722c9899 100644
--- a/src/Data/Vec/Membership/Propositional/Properties.agda
+++ b/src/Data/Vec/Membership/Propositional/Properties.agda
@@ -10,7 +10,7 @@ module Data.Vec.Membership.Propositional.Properties where
 
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Product as Prod using (_,_; ∃; _×_; -,_)
-open import Data.Vec hiding (here; there)
+open import Data.Vec.Base
 open import Data.Vec.Relation.Unary.Any using (here; there)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
index 9b2bea47b7..ddc4242496 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Core.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -12,8 +12,8 @@ open import Data.Empty
 open import Data.Nat using (ℕ; suc)
 import Data.Nat.Properties as ℕ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
+open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
-open import Data.Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
 open import Function.Base using (flip)
 open import Function.Bundles using (_⇔_; mk⇔)
diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
index d3c24ab42b..80a10442ef 100644
--- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
@@ -15,7 +15,7 @@ open import Data.Empty
 open import Data.Unit using (⊤; tt)
 open import Data.Product using (proj₁; proj₂)
 open import Data.Nat using (ℕ)
-open import Data.Vec using (Vec; []; _∷_)
+open import Data.Vec.Base using (Vec; []; _∷_)
 import Data.Vec.Relation.Binary.Lex.Strict as Strict
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
   using (Pointwise; []; _∷_; head; tail)
diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda
index 1c9f171d7b..fd6455da55 100644
--- a/src/Data/Vec/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda
@@ -16,7 +16,7 @@ import Data.List.Relation.Unary.Any as List
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
 open import Data.Product as Prod using (∃; ∃₂; _×_; _,_; proj₁; proj₂)
-open import Data.Vec hiding (here; there)
+open import Data.Vec.Base hiding (here; there)
 open import Data.Vec.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Vec.Membership.Propositional
   using (_∈_; mapWith∈; find; lose)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
index 3ea01b2c17..bad78c4da2 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Properties as ℕₚ using (≤′-trans)
 open import Data.Product.Base         using (_,_; _×_; proj₂)
 open import Data.List.Base            using (_∷_; [])
 open import Data.List.Kleene
-open import Data.Vec                  using (Vec)
+open import Data.Vec.Base             using (Vec)
 open import Function.Base using (_⟨_⟩_; flip)
 open import Relation.Unary
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
index eeacadb154..4f6607d663 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
@@ -18,7 +18,7 @@ open import Function.Base using (_⟨_⟩_)
 open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare)
 open import Data.Product.Base  using (_,_; _×_; proj₁; proj₂)
 open import Data.List.Kleene
-open import Data.Vec      using (Vec)
+open import Data.Vec.Base      using (Vec)
 
 import Data.Nat.Properties as ℕ-Prop
 import Relation.Binary.PropositionalEquality.Core as ≡
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
index c7ad6d6145..c4e1ef756b 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Properties    using (≤′-trans)
 open import Data.Nat.Induction
 open import Data.Product.Base      using (_×_; _,_; proj₁; proj₂; map₁)
 open import Data.List.Kleene
-open import Data.Vec               using (Vec)
+open import Data.Vec.Base          using (Vec)
 open import Function.Base using (_⟨_⟩_; flip)
 open import Induction.WellFounded
 open import Relation.Unary
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
index 59b99cf71b..604f02c533 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
@@ -13,8 +13,8 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
+open import Data.Vec.Base         using (Vec)
 open import Data.Product.Base     using (_,_)
-open import Data.Vec              using (Vec)
 open import Data.Nat              using (_<′_)
 open import Data.Nat.Induction
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
index 3d6e8c512f..4e3e672916 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
@@ -14,7 +14,7 @@ module Tactic.RingSolver.Core.Polynomial.Semantics
   where
 
 open import Data.Nat          using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
-open import Data.Vec          using (Vec; []; _∷_; uncons)
+open import Data.Vec.Base     using (Vec; []; _∷_; uncons)
 open import Data.List.Base    using ([]; _∷_)
 open import Data.Product.Base using (_,_; _×_)
 open import Data.List.Kleene  using (_+; _*; ∹_; _&_; [])
diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda
index ef99adc22e..6aa8997bb0 100644
--- a/src/Tactic/RingSolver/NonReflective.agda
+++ b/src/Tactic/RingSolver/NonReflective.agda
@@ -24,7 +24,7 @@ open import Data.Maybe.Base
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product
-open import Data.Vec hiding (_⊛_)
+open import Data.Vec.Base using (Vec)
 open import Data.Vec.N-ary
 
 open import Tactic.RingSolver.Core.Polynomial.Parameters