From 02dba8020fd65a81b1fd8d636b394f259695f672 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 23 Jan 2026 13:17:18 +0000
Subject: [PATCH 01/13] refactor: use `variable`s more systematically

---
 src/Data/List/Fresh.agda | 125 ++++++++++++++++++++-------------------
 1 file changed, 65 insertions(+), 60 deletions(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index c75d2edade..f8a49e018f 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -24,7 +24,7 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘′_; flip; id; _on_)
 open import Relation.Nullary using (does)
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Core using (Rel; REL)
 import Relation.Binary.Definitions as B using (Reflexive)
 open import Relation.Nary using (_⇒_; ∀[_])
 
@@ -34,6 +34,11 @@ private
     a b p r s : Level
     A : Set a
     B : Set b
+    P : Pred A p
+    R : Rel A r
+    S : Rel A s
+    x y : A
+
 
 ------------------------------------------------------------------------
 -- Basic type
@@ -44,11 +49,11 @@ private
 module _ {a} (A : Set a) (R : Rel A r) where
 
   data List# : Set (a ⊔ r)
-  fresh : (a : A) (as : List#) → Set r
+  fresh : REL A List# r
 
   data List# where
     []   : List#
-    cons : (a : A) (as : List#) → fresh a as → List#
+    cons : (x : A) (xs : List#) → fresh x xs → List#
 
   -- Whenever R can be reconstructed by η-expansion (e.g. because it is
   -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we
@@ -64,29 +69,29 @@ module _ {a} (A : Set a) (R : Rel A r) where
 
 -- Convenient notation for freshness making A and R implicit parameters
 infix 5 _#_
-_#_ : {R : Rel A r} (a : A) (as : List# A R) → Set r
+_#_ : REL A (List# A R) _
 _#_ = fresh _ _
 
 ------------------------------------------------------------------------
 -- Operations for modifying fresh lists
 
-module _ {R : Rel A r} {S : Rel B s} (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where
+module _ (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where
 
   map   : List# A R → List# B S
-  map-# : ∀ {a} as → a # as → f a # map as
+  map-# : ∀ xs → x # xs → f x # map xs
 
   map []             = []
-  map (cons a as ps) = cons (f a) (map as) (map-# as ps)
+  map (cons x xs ps) = cons (f x) (map xs) (map-# xs ps)
 
   map-# []        _        = _
-  map-# (a ∷# as) (p , ps) = R⇒S p , map-# as ps
+  map-# (x ∷# xs) (p , ps) = R⇒S p , map-# xs ps
 
-module _ {R : Rel B r} (f : A → B) where
+module _ (f : A → B) where
 
   map₁ : List# A (R on f) → List# B R
   map₁ = map f id
 
-module _ {R : Rel A r} {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where
+module _ {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where
 
   map₂ : List# A R → List# A S
   map₂ = map id R⇒S
@@ -94,115 +99,115 @@ module _ {R : Rel A r} {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where
 ------------------------------------------------------------------------
 -- Views
 
-data Empty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
+data Empty {A : Set a} {R : Rel A r} : Pred (List# A R) (a ⊔ r) where
   [] : Empty []
 
-data NonEmpty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
+data NonEmpty {A : Set a} {R : Rel A r} : Pred (List# A R) (a ⊔ r) where
   cons : ∀ x xs pr → NonEmpty (cons x xs pr)
 
 ------------------------------------------------------------------------
 -- Operations for reducing fresh lists
 
-length : {R : Rel A r} → List# A R → ℕ
+length : List# A R → ℕ
 length []        = 0
 length (_ ∷# xs) = suc (length xs)
 
 ------------------------------------------------------------------------
 -- Operations for constructing fresh lists
 
-pattern [_] a = a ∷# []
+pattern [_] x = x ∷# []
 
-fromMaybe : {R : Rel A r} → Maybe A → List# A R
+fromMaybe : Maybe A → List# A R
 fromMaybe nothing  = []
-fromMaybe (just a) = [ a ]
+fromMaybe (just x) = [ x ]
 
-module _ {R : Rel A r} (R-refl : B.Reflexive R) where
+module _ (R-refl : B.Reflexive {A = A} R) where
 
   replicate   : ℕ → A → List# A R
-  replicate-# : (n : ℕ) (a : A) → a # replicate n a
+  replicate-# : (n : ℕ) (x : A) → x # replicate n x
 
-  replicate zero    a = []
-  replicate (suc n) a = cons a (replicate n a) (replicate-# n a)
+  replicate zero    x = []
+  replicate (suc n) x = cons x (replicate n x) (replicate-# n x)
 
-  replicate-# zero    a = _
-  replicate-# (suc n) a = R-refl , replicate-# n a
+  replicate-# zero    x = _
+  replicate-# (suc n) x = R-refl , replicate-# n x
 
 ------------------------------------------------------------------------
 -- Operations for deconstructing fresh lists
 
-uncons : {R : Rel A r} → List# A R → Maybe (A × List# A R)
+uncons : List# A R → Maybe (A × List# A R)
 uncons []        = nothing
-uncons (a ∷# as) = just (a , as)
+uncons (x ∷# xs) = just (x , xs)
 
-head : {R : Rel A r} → List# A R → Maybe A
+head : List# A R → Maybe A
 head = Maybe.map proj₁ ∘′ uncons
 
-tail : {R : Rel A r} → List# A R → Maybe (List# A R)
+tail : List# A R → Maybe (List# A R)
 tail = Maybe.map proj₂ ∘′ uncons
 
-take   : {R : Rel A r} → ℕ → List# A R → List# A R
-take-# : {R : Rel A r} → ∀ n a (as : List# A R) → a # as → a # take n as
+take   : ℕ → List# A R → List# A R
+take-# : ∀ n y (xs : List# A R) → y # xs → y # take n xs
 
 take zero    xs             = []
 take (suc n) []             = []
-take (suc n) (cons a as ps) = cons a (take n as) (take-# n a as ps)
+take (suc n) (cons x xs ps) = cons x (take n xs) (take-# n x xs ps)
 
-take-# zero    a xs        _        = _
-take-# (suc n) a []        ps       = _
-take-# (suc n) a (x ∷# xs) (p , ps) = p , take-# n a xs ps
+take-# zero    y xs        _        = _
+take-# (suc n) y []        ps       = _
+take-# (suc n) y (x ∷# xs) (p , ps) = p , take-# n y xs ps
 
-drop : {R : Rel A r} → ℕ → List# A R → List# A R
-drop zero    as        = as
+drop : ℕ → List# A R → List# A R
+drop zero    xs        = xs
 drop (suc n) []        = []
-drop (suc n) (a ∷# as) = drop n as
+drop (suc n) (x ∷# xs) = drop n xs
 
-module _ {P : Pred A p} (P? : U.Decidable P) where
+module _ (P? : U.Decidable {A = A} P) where
 
-  takeWhile   : {R : Rel A r} → List# A R → List# A R
-  takeWhile-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # takeWhile as
+  takeWhile   : List# A R → List# A R
+  takeWhile-# : ∀ y (xs : List# A R) → y # xs → y # takeWhile xs
 
   takeWhile []             = []
-  takeWhile (cons a as ps) =
-    if does (P? a) then cons a (takeWhile as) (takeWhile-# a as ps) else []
+  takeWhile (cons x xs ps) =
+    if does (P? x) then cons x (takeWhile xs) (takeWhile-# x xs ps) else []
 
   -- this 'with' is needed to cause reduction in the type of 'takeWhile (a ∷# as)'
-  takeWhile-# a []        _        = _
-  takeWhile-# a (x ∷# xs) (p , ps) with does (P? x)
-  ... | true  = p , takeWhile-# a xs ps
+  takeWhile-# y []        _        = _
+  takeWhile-# y (x ∷# xs) (p , ps) with does (P? x)
+  ... | true  = p , takeWhile-# y xs ps
   ... | false = _
 
-  dropWhile : {R : Rel A r} → List# A R → List# A R
+  dropWhile : List# A R → List# A R
   dropWhile []            = []
-  dropWhile aas@(a ∷# as)  = if does (P? a) then dropWhile as else aas
+  dropWhile xxs@(x ∷# xs)  = if does (P? x) then dropWhile xs else xxs
 
-  filter   : {R : Rel A r} → List# A R → List# A R
-  filter-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # filter as
+  filter   : List# A R → List# A R
+  filter-# : ∀ y (xs : List# A R) → y # xs → y # filter xs
 
   filter []             = []
-  filter (cons a as ps) =
-    let l = filter as in
-    if does (P? a) then cons a l (filter-# a as ps) else l
+  filter (cons x xs ps) =
+    let l = filter xs in
+    if does (P? x) then cons x l (filter-# x xs ps) else l
 
-  -- this 'with' is needed to cause reduction in the type of 'filter-# a (x ∷# xs)'
-  filter-# a []        _        = _
-  filter-# a (x ∷# xs) (p , ps) with does (P? x)
-  ... | true  = p , filter-# a xs ps
-  ... | false = filter-# a xs ps
+  -- this 'with' is needed to cause reduction in the type of 'filter-# y (x ∷# xs)'
+  filter-# y []        _        = _
+  filter-# y (x ∷# xs) (p , ps) with does (P? x)
+  ... | true  = p , filter-# y xs ps
+  ... | false = filter-# y xs ps
 
 ------------------------------------------------------------------------
 -- Relationship to List and AllPairs
 
-toList : {R : Rel A r} → List# A R → ∃ (AllPairs R)
-toAll  : ∀ {R : Rel A r} {a} as → fresh A R a as → All (R a) (proj₁ (toList as))
+toList : List# A R → ∃ (AllPairs R)
+toAll  : (xs : List# A R) → x # xs → All (R x) (proj₁ (toList xs))
 
 toList []             = -, []
 toList (cons x xs ps) = -, toAll xs ps ∷ proj₂ (toList xs)
 
 toAll []        ps       = []
-toAll (a ∷# as) (p , ps) = p ∷ toAll as ps
+toAll (x ∷# xs) (p , ps) = p ∷ toAll xs ps
 
-fromList   : ∀ {R : Rel A r} {xs} → AllPairs R xs → List# A R
-fromList-# : ∀ {R : Rel A r} {x xs} (ps : AllPairs R xs) →
+fromList   : ∀ {xs} → AllPairs R xs → List# A R
+fromList-# : ∀ {xs} (ps : AllPairs R xs) →
              All (R x) xs → x # fromList ps
 
 fromList []       = []

From 67ef7e19a0c83e5bfd0e760dc85858745db91725 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 27 Jan 2026 11:57:40 +0000
Subject: [PATCH 02/13] refactor: remove `P` from `variable` block

---
 src/Data/List/Fresh.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index f8a49e018f..29a1ae4d2e 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -34,7 +34,6 @@ private
     a b p r s : Level
     A : Set a
     B : Set b
-    P : Pred A p
     R : Rel A r
     S : Rel A s
     x y : A
@@ -161,7 +160,7 @@ drop zero    xs        = xs
 drop (suc n) []        = []
 drop (suc n) (x ∷# xs) = drop n xs
 
-module _ (P? : U.Decidable {A = A} P) where
+module _ {P : Pred A p} (P? : U.Decidable {A = A} P) where
 
   takeWhile   : List# A R → List# A R
   takeWhile-# : ∀ y (xs : List# A R) → y # xs → y # takeWhile xs

From 6af45e404a147870b0e7e5504cfa4c1aecd6ed16 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 27 Jan 2026 18:08:07 +0000
Subject: [PATCH 03/13] refactor: `Properties` follow easily

---
 src/Data/List/Fresh/Properties.agda | 32 +++++++++++++++--------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/src/Data/List/Fresh/Properties.agda b/src/Data/List/Fresh/Properties.agda
index 1f39b1d057..7d8ae09aec 100644
--- a/src/Data/List/Fresh/Properties.agda
+++ b/src/Data/List/Fresh/Properties.agda
@@ -11,42 +11,44 @@ module Data.List.Fresh.Properties where
 open import Data.List.Fresh using (List#; _∷#_; _#_; Empty; NonEmpty; cons; [])
 open import Data.Product.Base using (_,_)
 open import Level using (Level; _⊔_)
+open import Relation.Binary.Definitions as Binary using (_Respects_; _Respectsˡ_)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Nullary.Negation using (¬_)
-open import Relation.Unary as U using (Pred)
-import Relation.Binary.Definitions as B using (_Respectsˡ_; Irrelevant)
-open import Relation.Binary.Core using (Rel)
-
 
 private
   variable
-    a b e p r : Level
+    a b ℓ p r : Level
     A : Set a
     B : Set b
+    R : Rel A r
+    x y : A
+    xs : List# A R
+
 
 ------------------------------------------------------------------------
 -- Fresh congruence
 
-module _ {R : Rel A r} {_≈_ : Rel A e} (R≈ : R B.Respectsˡ _≈_) where
+module _ {_≈_ : Rel A ℓ} (resp : R Respectsˡ _≈_) where
 
-  fresh-respectsˡ : ∀ {x y} {xs : List# A R} → x ≈ y → x # xs → y # xs
-  fresh-respectsˡ {xs = []}      x≈y x#xs       = _
+  fresh-respectsˡ : ∀ {xs : List# A R} → (_# xs) Respects _≈_
+  fresh-respectsˡ {xs = []}      x≈y _          = _
   fresh-respectsˡ {xs = x ∷# xs} x≈y (r , x#xs) =
-    R≈ x≈y r , fresh-respectsˡ x≈y x#xs
+    resp x≈y r , fresh-respectsˡ x≈y x#xs
 
 ------------------------------------------------------------------------
 -- Empty and NotEmpty
 
-Empty⇒¬NonEmpty : {R : Rel A r} {xs : List# A R} → Empty xs → ¬ (NonEmpty xs)
+Empty⇒¬NonEmpty : Empty xs → ¬ (NonEmpty xs)
 Empty⇒¬NonEmpty [] ()
 
-NonEmpty⇒¬Empty : {R : Rel A r} {xs : List# A R} → NonEmpty xs → ¬ (Empty xs)
+NonEmpty⇒¬Empty : NonEmpty xs → ¬ (Empty xs)
 NonEmpty⇒¬Empty () []
 
-empty? : {R : Rel A r} (xs : List# A R) → Dec (Empty xs)
+empty? : (xs : List# A R) → Dec (Empty xs)
 empty? []       = yes []
-empty? (_ ∷# _) = no (λ ())
+empty? (_ ∷# _) = no λ()
 
-nonEmpty? : {R : Rel A r} (xs : List# A R) → Dec (NonEmpty xs)
-nonEmpty? []             = no (λ ())
+nonEmpty? : (xs : List# A R) → Dec (NonEmpty xs)
+nonEmpty? []             = no λ()
 nonEmpty? (cons x xs pr) = yes (cons x xs pr)

From de98e4ed907424ce667639af3e28b6ba596ba06b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jan 2026 11:10:53 +0000
Subject: [PATCH 04/13] refactor: propagate the `variable` style throughout

---
 src/Data/List/Fresh/Membership/Setoid.agda    | 18 ++--
 .../Fresh/Membership/Setoid/Properties.agda   | 89 +++++++++----------
 src/Data/List/Fresh/Relation/Unary/All.agda   | 67 +++++++-------
 .../Fresh/Relation/Unary/All/Properties.agda  | 31 ++++---
 src/Data/List/Fresh/Relation/Unary/Any.agda   | 47 +++++-----
 5 files changed, 125 insertions(+), 127 deletions(-)

diff --git a/src/Data/List/Fresh/Membership/Setoid.agda b/src/Data/List/Fresh/Membership/Setoid.agda
index 6be37629d7..b5d52b397c 100644
--- a/src/Data/List/Fresh/Membership/Setoid.agda
+++ b/src/Data/List/Fresh/Membership/Setoid.agda
@@ -10,22 +10,26 @@ open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Fresh.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
-open import Level using (Level; _⊔_)
+open import Level using (Level)
 open import Data.List.Fresh using (List#)
 open import Data.List.Fresh.Relation.Unary.Any as Any using (Any)
-open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Core using (Rel; REL)
 open import Relation.Nullary.Negation.Core using (¬_)
 
-open Setoid S renaming (Carrier to A)
-
-infix 4 _∈_ _∉_
+open Setoid S
+  using (_≈_)
+  renaming (Carrier to A)
 
 private
   variable
     r : Level
+    R : Rel A r
+
+
+infix 4 _∈_ _∉_
 
-_∈_ : {R : Rel A r} → A → List# A R → Set _
+_∈_ : REL A (List# A R) _
 x ∈ xs = Any (x ≈_) xs
 
-_∉_ : {R : Rel A r} → A → List# A R → Set _
+_∉_ : REL A (List# A R) _
 x ∉ xs = ¬ (x ∈ xs)
diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
index 819ee4a893..cf873d61d6 100644
--- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
@@ -8,104 +8,99 @@
 
 open import Relation.Binary.Bundles using (Setoid)
 
-module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ)
+module Data.List.Fresh.Membership.Setoid.PropertiesJHM {c ℓ} (S : Setoid c ℓ)
   where
 
-open import Level using (Level; _⊔_)
+open import Level using (Level)
 open import Data.List.Fresh
 open import Data.List.Fresh.Properties using (fresh-respectsˡ)
 open import Data.List.Fresh.Membership.Setoid S using (_∈_; _∉_)
 open import Data.List.Fresh.Relation.Unary.Any using (Any; here; there; _─_)
-import Data.List.Fresh.Relation.Unary.Any.Properties as List#
+open import Data.List.Fresh.Relation.Unary.Any.Properties as List#
   using (length-remove)
-open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; suc; zero; _≤_; _<_; z≤n; s≤s; z<s; s<s)
 open import Data.Nat.Properties using (module ≤-Reasoning)
 open import Data.Product.Base using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂)
 open import Function.Base using (id; _∘′_; _$_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.Definitions as Binary using (_Respectsˡ_)
+open import Relation.Binary.PropositionalEquality.Core as ≡
+  using (cong)
+open import Relation.Nary using (∀[_]; _⇒_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction′)
 open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Unary as Unary using (Pred)
-import Relation.Binary.Definitions as Binary using (_Respectsˡ_; Irrelevant)
-import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_; cong; sym; subst)
-open import Relation.Nary using (∀[_]; _⇒_)
-open import Relation.Nullary.Negation.Core using (contradiction)
 
 open Setoid S renaming (Carrier to A)
 
 private
   variable
-    p r : Level
+    r : Level
+    R : Rel A r
+    x y : A
+    xs : List# A R
+
 
 ------------------------------------------------------------------------
 -- transport
 
-module _ {R : Rel A r} where
-
-  ≈-subst-∈ : ∀ {x y} {xs : List# A R} → x ≈ y → x ∈ xs → y ∈ xs
-  ≈-subst-∈ x≈y (here x≈x′)  = here (trans (sym x≈y) x≈x′)
-  ≈-subst-∈ x≈y (there x∈xs) = there (≈-subst-∈ x≈y x∈xs)
+≈-subst-∈ : x ≈ y → x ∈ xs → y ∈ xs
+≈-subst-∈ x≈y (here x≈x′)  = here (trans (sym x≈y) x≈x′)
+≈-subst-∈ x≈y (there x∈xs) = there (≈-subst-∈ x≈y x∈xs)
 
 ------------------------------------------------------------------------
 -- relationship to fresh
 
-module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where
+module _ (R⇒≉ : ∀[ R ⇒ _≉_ ]) where
 
-  fresh⇒∉ : ∀ {x} {xs : List# A R} → x # xs → x ∉ xs
+  fresh⇒∉ : ∀ {xs : List# A R} → x # xs → x ∉ xs
   fresh⇒∉ (r , _)    (here x≈y)   = R⇒≉ r x≈y
   fresh⇒∉ (_ , x#xs) (there x∈xs) = fresh⇒∉ x#xs x∈xs
 
 ------------------------------------------------------------------------
 -- disjointness
 
-module _ {R : Rel A r} where
-
-  distinct : ∀ {x y} {xs : List# A R} → x ∈ xs → y ∉ xs → x ≉ y
-  distinct x∈xs y∉xs x≈y = y∉xs (≈-subst-∈ x≈y x∈xs)
+distinct : x ∈ xs → y ∉ xs → x ≉ y
+distinct x∈xs y∉xs x≈y = y∉xs (≈-subst-∈ x≈y x∈xs)
 
 ------------------------------------------------------------------------
 -- remove
 
-module _ {R : Rel A r} where
-
-  remove-inv : ∀ {x y} {xs : List# A R} (x∈xs : x ∈ xs) →
-               y ∈ xs → x ≈ y ⊎ y ∈ (xs ─ x∈xs)
-  remove-inv (here x≈z)   (here y≈z)   = inj₁ (trans x≈z (sym y≈z))
-  remove-inv (here _)     (there y∈xs) = inj₂ y∈xs
-  remove-inv (there _)    (here y≈z)   = inj₂ (here y≈z)
-  remove-inv (there x∈xs) (there y∈xs) = Sum.map₂ there (remove-inv x∈xs y∈xs)
+remove-inv : (x∈xs : x ∈ xs) → y ∈ xs → x ≈ y ⊎ y ∈ (xs ─ x∈xs)
+remove-inv (here x≈z)   (here y≈z)   = inj₁ (trans x≈z (sym y≈z))
+remove-inv (here _)     (there y∈xs) = inj₂ y∈xs
+remove-inv (there _)    (here y≈z)   = inj₂ (here y≈z)
+remove-inv (there x∈xs) (there y∈xs) = Sum.map₂ there (remove-inv x∈xs y∈xs)
 
-  ∈-remove : ∀ {x y} {xs : List# A R} (x∈xs : x ∈ xs) → y ∈ xs → x ≉ y → y ∈ (xs ─ x∈xs)
-  ∈-remove x∈xs y∈xs x≉y = fromInj₂ (⊥-elim ∘′ x≉y) (remove-inv x∈xs y∈xs)
+∈-remove : (x∈xs : x ∈ xs) → y ∈ xs → x ≉ y → y ∈ (xs ─ x∈xs)
+∈-remove x∈xs y∈xs x≉y = fromInj₂ (contradiction′ x≉y) (remove-inv x∈xs y∈xs)
 
-module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≉⇒R : ∀[ _≉_ ⇒ R ]) where
+module _ (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≉⇒R : ∀[ _≉_ ⇒ R ]) where
 
   private
     R≈ : R Binary.Respectsˡ _≈_
     R≈ x≈y Rxz = ≉⇒R (R⇒≉ Rxz ∘′ trans x≈y)
 
-  fresh-remove : ∀ {x} {xs : List# A R} (x∈xs : x ∈ xs) → x # (xs ─ x∈xs)
+  fresh-remove : ∀ {xs : List# A R} (x∈xs : x ∈ xs) → x # (xs ─ x∈xs)
   fresh-remove {xs = cons x xs pr} (here x≈y)   = fresh-respectsˡ R≈ (sym x≈y) pr
   fresh-remove {xs = cons x xs pr} (there x∈xs) =
     ≉⇒R (distinct x∈xs (fresh⇒∉ R⇒≉ pr)) , fresh-remove x∈xs
 
-  ∉-remove : ∀ {x} {xs : List# A R} (x∈xs : x ∈ xs) → x ∉ (xs ─ x∈xs)
+  ∉-remove : ∀ {xs : List# A R} (x∈xs : x ∈ xs) → x ∉ (xs ─ x∈xs)
   ∉-remove x∈xs = fresh⇒∉ R⇒≉ (fresh-remove x∈xs)
 
 ------------------------------------------------------------------------
 -- injection
 
-module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where
+module _ (R⇒≉ : ∀[ R ⇒ _≉_ ]) where
 
   injection : ∀ {xs ys : List# A R} (inj : ∀ {x} → x ∈ xs → x ∈ ys) →
               length xs ≤ length ys
   injection {[]}                 {ys} inj = z≤n
   injection {xxs@(cons x xs pr)} {ys} inj = begin
     length xxs               ≤⟨ s≤s (injection step) ⟩
-    suc (length (ys ─ x∈ys)) ≡⟨ ≡.sym (List#.length-remove x∈ys) ⟩
+    suc (length (ys ─ x∈ys)) ≡⟨ length-remove x∈ys ⟨
     length ys                ∎
 
     where
@@ -118,34 +113,34 @@ module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where
     x∈ys : x ∈ ys
     x∈ys = inj (here refl)
 
-    step : ∀ {y} → y ∈ xs → y ∈ (ys ─ x∈ys)
-    step {y} y∈xs = ∈-remove x∈ys (inj (there y∈xs)) (distinct y∈xs x∉xs ∘′ sym)
+    step : y ∈ xs → y ∈ (ys ─ x∈ys)
+    step y∈xs = ∈-remove x∈ys (inj (there y∈xs)) (distinct y∈xs x∉xs ∘′ sym)
 
   strict-injection : ∀ {xs ys : List# A R} (inj : ∀ {x} → x ∈ xs → x ∈ ys) →
    (∃ λ x → x ∈ ys × x ∉ xs) → length xs < length ys
   strict-injection {xs} {ys} inj (x , x∈ys , x∉xs) = begin
     suc (length xs)          ≤⟨ s≤s (injection step) ⟩
-    suc (length (ys ─ x∈ys)) ≡⟨ ≡.sym (List#.length-remove x∈ys) ⟩
+    suc (length (ys ─ x∈ys)) ≡⟨ length-remove x∈ys ⟨
     length ys                ∎
 
     where
 
     open ≤-Reasoning
 
-    step : ∀ {y} → y ∈ xs → y ∈ (ys ─ x∈ys)
-    step {y} y∈xs = fromInj₂ (λ x≈y → contradiction ((≈-subst-∈ (sym x≈y) y∈xs)) x∉xs)
-                  $ remove-inv x∈ys (inj y∈xs)
+    step : y ∈ xs → y ∈ (ys ─ x∈ys)
+    step y∈xs = fromInj₂ (λ x≈y → contradiction ((≈-subst-∈ (sym x≈y) y∈xs)) x∉xs)
+                $ remove-inv x∈ys (inj y∈xs)
 
 
 ------------------------------------------------------------------------
 -- proof irrelevance
 
-module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≈-irrelevant : Binary.Irrelevant _≈_) where
+module _ (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≈-irrelevant : Binary.Irrelevant _≈_) where
 
-  ∈-irrelevant : ∀ {x} {xs : List# A R} → Irrelevant (x ∈ xs)
+  ∈-irrelevant : ∀ {xs : List# A R} → Irrelevant (x ∈ xs)
   -- positive cases
-  ∈-irrelevant (here x≈y₁)   (here x≈y₂)   = ≡.cong here (≈-irrelevant x≈y₁ x≈y₂)
-  ∈-irrelevant (there x∈xs₁) (there x∈xs₂) = ≡.cong there (∈-irrelevant x∈xs₁ x∈xs₂)
+  ∈-irrelevant (here x≈y₁)   (here x≈y₂)   = cong here (≈-irrelevant x≈y₁ x≈y₂)
+  ∈-irrelevant (there x∈xs₁) (there x∈xs₂) = cong there (∈-irrelevant x∈xs₁ x∈xs₂)
   -- absurd cases
   ∈-irrelevant {xs = cons x xs pr} (here x≈y)    (there x∈xs₂) =
     contradiction x≈y (distinct x∈xs₂ (fresh⇒∉ R⇒≉ pr))
diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda
index fffe091c24..03cfc59e58 100644
--- a/src/Data/List/Fresh/Relation/Unary/All.agda
+++ b/src/Data/List/Fresh/Relation/Unary/All.agda
@@ -14,8 +14,8 @@ open import Data.Product.Base using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘_; _$_)
 open import Level using (Level; _⊔_; Lift)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×?_)
-open import Relation.Unary as U
+open import Relation.Nullary.Decidable.Core as Dec using (Dec; yes; no; _×?_)
+open import Relation.Unary as Unary
   using (Pred; IUniversal; Universal; Decidable; _⇒_; _∪_; _∩_)
 open import Relation.Binary.Core using (Rel)
 
@@ -24,6 +24,12 @@ private
   variable
     a p q r : Level
     A : Set a
+    R : Rel A r
+    P : Pred A p
+    Q : Pred A q
+    x : A
+    xs : List# A R
+
 
 module _ {A : Set a} {R : Rel A r} (P : Pred A p) where
 
@@ -33,50 +39,41 @@ module _ {A : Set a} {R : Rel A r} (P : Pred A p) where
     []  : All []
     _∷_ : ∀ {x xs pr} → P x → All xs → All (cons x xs pr)
 
-module _ {R : Rel A r} {P : Pred A p} where
-
-  uncons : ∀ {x} {xs : List# A R} {pr} →
-           All P (cons x xs pr) → P x × All P xs
-  uncons (p ∷ ps) = p , ps
 
-module _ {R : Rel A r} where
+uncons : ∀ {pr} → All P (cons x xs pr) → P x × All P xs
+uncons (p ∷ ps) = p , ps
 
-  append   : (xs ys : List# A R) → All (_# ys) xs → List# A R
-  append-# : ∀ {x} xs ys {ps} → x # xs → x # ys → x # append xs ys ps
+append   : (xs ys : List# A R) → All (_# ys) xs → List# A R
+append-# : ∀ xs ys {ps} → x # xs → x # ys → x # append {R = R} xs ys ps
 
-  append []             ys _  = ys
-  append (cons x xs pr) ys ps =
-    let (p , ps) = uncons ps in
-    cons x (append xs ys ps) (append-# xs ys pr p)
+append []             ys _  = ys
+append (cons x xs pr) ys ps =
+  let (p , ps) = uncons ps in
+  cons x (append xs ys ps) (append-# xs ys pr p)
 
-  append-# []             ys x#xs       x#ys = x#ys
-  append-# (cons x xs pr) ys (r , x#xs) x#ys = r , append-# xs ys x#xs x#ys
+append-# []             ys x#xs       x#ys = x#ys
+append-# (cons x xs pr) ys (r , x#xs) x#ys = r , append-# xs ys x#xs x#ys
 
-module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} where
+map : ∀[ P ⇒ Q ] → All P xs → All Q xs
+map p⇒q []       = []
+map p⇒q (p ∷ ps) = p⇒q p ∷ map p⇒q ps
 
-  map : ∀ {xs : List# A R} → ∀[ P ⇒ Q ] → All P xs → All Q xs
-  map p⇒q []       = []
-  map p⇒q (p ∷ ps) = p⇒q p ∷ map p⇒q ps
+lookup : All Q xs → (ps : Any P xs) → Q (proj₁ (Any.witness ps))
+lookup (q ∷ _)  (here _)  = q
+lookup (_ ∷ qs) (there k) = lookup qs k
 
-  lookup : ∀ {xs : List# A R} → All Q xs → (ps : Any P xs) →
-           Q (proj₁ (Any.witness ps))
-  lookup (q ∷ _)  (here _)  = q
-  lookup (_ ∷ qs) (there k) = lookup qs k
+module _ (P? : Decidable P) where
 
-module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
-
-  all? : (xs : List# A R) → Dec (All P xs)
+  all? : ∀ xs → Dec (All {R = R} P xs)
   all? []        = yes []
   all? (x ∷# xs) = Dec.map′ (uncurry _∷_) uncons (P? x ×? all? xs)
 
 ------------------------------------------------------------------------
 -- Generalised decidability procedure
 
-module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} where
-
-  decide :  Π[ P ∪ Q ] → Π[ All {R = R} P ∪ Any Q ]
-  decide p∪q [] = inj₁ []
-  decide p∪q (x ∷# xs) =
-    [ (λ px → Sum.map (px ∷_) there (decide p∪q xs))
-    , inj₂ ∘ here
-    ]′ $ p∪q x
+decide :  Π[ P ∪ Q ] → Π[ All {R = R} P ∪ Any Q ]
+decide p∪q [] = inj₁ []
+decide p∪q (x ∷# xs) =
+  [ (λ px → Sum.map (px ∷_) there (decide p∪q xs))
+  , inj₂ ∘ here
+  ]′ $ p∪q x
diff --git a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
index e6f1d5e556..41b41cde68 100644
--- a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
@@ -14,30 +14,29 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘′_)
 open import Level using (Level; _⊔_; Lift)
-open import Relation.Unary  as U using (Pred)
+open import Relation.Unary  as Unary using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
-
-
 private
   variable
     a p r : Level
     A : Set a
+    R : Rel A r
+    P : Pred A p
+    x : A
+    xs ys : List# A R
 
-module _ {R : Rel A r} where
-
-  fromAll : ∀ {x} {xs : List# A R} → All (R x) xs → x # xs
-  fromAll []       = _
-  fromAll (p ∷ ps) = p , fromAll ps
 
-  toAll : ∀ {x} {xs : List# A R} → x # xs → All (R x) xs
-  toAll {xs = []}      _        = []
-  toAll {xs = a ∷# as} (p , ps) = p ∷ toAll ps
+fromAll : All {R = R} (R x) xs → x # xs
+fromAll []       = _
+fromAll (p ∷ ps) = p , fromAll ps
 
-module _ {R : Rel A r} {P : Pred A p} where
+toAll : x # xs → All {R = R} (R x) xs
+toAll {xs = []}      _        = []
+toAll {xs = a ∷# as} (p , ps) = p ∷ toAll ps
 
-  append⁺ : {xs ys : List# A R} {ps : All (_# ys) xs} →
-            All P xs → All P ys → All P (append xs ys ps)
-  append⁺ []         pys = pys
-  append⁺ (px ∷ pxs) pys = px ∷ append⁺ pxs pys
+append⁺ : {ps : All {R = R} (_# ys) xs} →
+          All P xs → All P ys → All P (append xs ys ps)
+append⁺ []         pys = pys
+append⁺ (px ∷ pxs) pys = px ∷ append⁺ pxs pys
diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda
index e86379f3ac..ad5f654215 100644
--- a/src/Data/List/Fresh/Relation/Unary/Any.agda
+++ b/src/Data/List/Fresh/Relation/Unary/Any.agda
@@ -9,20 +9,27 @@
 module Data.List.Fresh.Relation.Unary.Any where
 
 open import Level using (Level; _⊔_; Lift)
-open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
+open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_; fresh)
 open import Data.Product.Base using (∃; _,_; -,_)
 open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Nullary.Decidable as Dec using (Dec; no; _⊎?_)
-open import Relation.Unary  as U using (Pred; IUniversal; Universal; Decidable; _⇒_; _∪_; _∩_)
+open import Relation.Unary as Unary
+  using (Pred; IUniversal; Universal; Decidable; _⇒_; _∪_; _∩_)
 open import Relation.Binary.Core using (Rel)
 
 private
   variable
     a p q r : Level
     A : Set a
+    R : Rel A r
+    P : Pred A p
+    Q : Pred A q
+    x : A
+    xs : List# A R
+
 
 module _ {A : Set a} {R : Rel A r} (P : Pred A p) where
 
@@ -30,7 +37,7 @@ module _ {A : Set a} {R : Rel A r} (P : Pred A p) where
     here  : ∀ {x xs pr} → P x → Any (cons x xs pr)
     there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)
 
-module _ {R : Rel A r} {P : Pred A p} {x} {xs : List# A R} {pr} where
+module _ {pr : fresh A R x xs} where
 
   head : ¬ Any P xs → Any P (cons x xs pr) → P x
   head ¬tail (here p)   = p
@@ -50,32 +57,28 @@ module _ {R : Rel A r} {P : Pred A p} {x} {xs : List# A R} {pr} where
   ⊎⇔Any : (P x ⊎ Any P xs) ⇔ Any P (cons x xs pr)
   ⊎⇔Any = mk⇔ fromSum toSum
 
-module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} where
-
-  map : {xs : List# A R} → ∀[ P ⇒ Q ] → Any P xs → Any Q xs
-  map p⇒q (here p)  = here (p⇒q p)
-  map p⇒q (there p) = there (map p⇒q p)
-
-module _ {R : Rel A r} {P : Pred A p} where
+map : ∀[ P ⇒ Q ] → Any P xs → Any Q xs
+map p⇒q (here p)  = here (p⇒q p)
+map p⇒q (there p) = there (map p⇒q p)
 
-  witness : {xs : List# A R} → Any P xs → ∃ P
-  witness (here p)   = -, p
-  witness (there ps) = witness ps
+witness : Any P xs → ∃ P
+witness (here p)   = -, p
+witness (there ps) = witness ps
 
-  remove   : (xs : List# A R) → Any P xs → List# A R
-  remove-# : ∀ {x} {xs : List# A R} p → x # xs → x # (remove xs p)
+remove   : (xs : List# A R) → Any P xs → List# A R
+remove-# : (p : Any {R = R} P xs) → x # xs → x # (remove xs p)
 
-  remove (_ ∷# xs)      (here _)  = xs
-  remove (cons x xs pr) (there k) = cons x (remove xs k) (remove-# k pr)
+remove (_ ∷# xs)      (here _)  = xs
+remove (cons x xs pr) (there k) = cons x (remove xs k) (remove-# k pr)
 
-  remove-# (here x)  (p , ps) = ps
-  remove-# (there k) (p , ps) = p , remove-# k ps
+remove-# (here x)  (p , ps) = ps
+remove-# (there k) (p , ps) = p , remove-# k ps
 
 infixl 4 _─_
 _─_ = remove
 
-module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
+module _ (P? : Decidable P) where
 
-  any? : (xs : List# A R) → Dec (Any P xs)
-  any? []        = no (λ ())
+  any? : ∀ xs → Dec (Any {R = R} P xs)
+  any? []        = no λ()
   any? (x ∷# xs) = Dec.map ⊎⇔Any (P? x ⊎? any? xs)

From c20a2c32e8bb141ba4dcb5a573c4b28a5e1e6ebf Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 28 Jan 2026 11:12:10 +0000
Subject: [PATCH 05/13] Update src/Data/List/Fresh.agda

---
 src/Data/List/Fresh.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index 29a1ae4d2e..35a17fd045 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -23,7 +23,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘′_; flip; id; _on_)
 open import Relation.Nullary using (does)
-open import Relation.Unary as U using (Pred)
+open import Relation.Unary as Unary using (Pred; Decidable)
 open import Relation.Binary.Core using (Rel; REL)
 import Relation.Binary.Definitions as B using (Reflexive)
 open import Relation.Nary using (_⇒_; ∀[_])

From 2d081b66316b7e426897822a51250d00beed25f5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 28 Jan 2026 11:34:57 +0000
Subject: [PATCH 06/13] Update src/Data/List/Fresh.agda

---
 src/Data/List/Fresh.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index 35a17fd045..6d2458c851 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -120,7 +120,7 @@ fromMaybe : Maybe A → List# A R
 fromMaybe nothing  = []
 fromMaybe (just x) = [ x ]
 
-module _ (R-refl : B.Reflexive {A = A} R) where
+module _ (refl : Reflexive {A = A} R) where
 
   replicate   : ℕ → A → List# A R
   replicate-# : (n : ℕ) (x : A) → x # replicate n x

From 09c8b5f5ef2bcfeff1f22bb4c22ba8c1b39c9134 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 28 Jan 2026 11:35:15 +0000
Subject: [PATCH 07/13] Update src/Data/List/Fresh.agda

---
 src/Data/List/Fresh.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index 6d2458c851..5c351751ed 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -129,7 +129,7 @@ module _ (refl : Reflexive {A = A} R) where
   replicate (suc n) x = cons x (replicate n x) (replicate-# n x)
 
   replicate-# zero    x = _
-  replicate-# (suc n) x = R-refl , replicate-# n x
+  replicate-# (suc n) x = refl , replicate-# n x
 
 ------------------------------------------------------------------------
 -- Operations for deconstructing fresh lists

From 502c9033d0a787b038268bb47a62a5bd206ba756 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 28 Jan 2026 11:35:53 +0000
Subject: [PATCH 08/13] Update src/Data/List/Fresh.agda

---
 src/Data/List/Fresh.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index 5c351751ed..4fdfa5659f 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -160,7 +160,7 @@ drop zero    xs        = xs
 drop (suc n) []        = []
 drop (suc n) (x ∷# xs) = drop n xs
 
-module _ {P : Pred A p} (P? : U.Decidable {A = A} P) where
+module _ {P : Pred A p} (P? : Decidable P) where
 
   takeWhile   : List# A R → List# A R
   takeWhile-# : ∀ y (xs : List# A R) → y # xs → y # takeWhile xs

From 563ad4b7fefc70cac546c5227ac8ff3cdc846e26 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jan 2026 11:38:18 +0000
Subject: [PATCH 09/13] fix: module name

---
 src/Data/List/Fresh/Membership/Setoid/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
index cf873d61d6..398bfdf6d5 100644
--- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
@@ -8,7 +8,7 @@
 
 open import Relation.Binary.Bundles using (Setoid)
 
-module Data.List.Fresh.Membership.Setoid.PropertiesJHM {c ℓ} (S : Setoid c ℓ)
+module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ)
   where
 
 open import Level using (Level)

From 0acb35e3f0d65b45847f0abce1aded3ef5a0d8ed Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jan 2026 11:48:58 +0000
Subject: [PATCH 10/13] fix: bug in `import`s

---
 src/Data/List/Fresh.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index 4fdfa5659f..9d9d2bf594 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -25,7 +25,7 @@ open import Function.Base using (_∘′_; flip; id; _on_)
 open import Relation.Nullary using (does)
 open import Relation.Unary as Unary using (Pred; Decidable)
 open import Relation.Binary.Core using (Rel; REL)
-import Relation.Binary.Definitions as B using (Reflexive)
+open import Relation.Binary.Definitions as Binary using (Reflexive)
 open import Relation.Nary using (_⇒_; ∀[_])
 
 

From cfc60a62c75fced398d6679e24428ffbe3cbc6b7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jan 2026 12:22:02 +0000
Subject: [PATCH 11/13] refactor: `Any.Properties`s

---
 .../Fresh/Relation/Unary/Any/Properties.agda  | 60 +++++++++----------
 1 file changed, 28 insertions(+), 32 deletions(-)

diff --git a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
index 1618295ece..d60073f426 100644
--- a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
@@ -19,7 +19,7 @@ open import Function.Base using (_∘′_)
 open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary.Decidable.Core
-open import Relation.Unary  as U using (Pred)
+open import Relation.Unary as Unary using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nary using (∀[_]; _⇒_; ∁; Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
@@ -30,37 +30,40 @@ private
     a b p q r s : Level
     A : Set a
     B : Set b
+    P : Pred A p
+    Q : Pred A q
+    R : Rel A r
+    xs ys : List# A R
+
 
 ------------------------------------------------------------------------
 -- NonEmpty
 
-module _ {R : Rel A r} {P : Pred A p} where
-
-  Any⇒NonEmpty : {xs : List# A R} → Any P xs → NonEmpty xs
-  Any⇒NonEmpty {xs = cons x xs pr} p  = cons x xs pr
+Any⇒NonEmpty : Any P xs → NonEmpty xs
+Any⇒NonEmpty {xs = cons x xs pr} p  = cons x xs pr
 
 ------------------------------------------------------------------------
 -- Correspondence between Any and All
 
-module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} (P⇒¬Q : ∀[ P ⇒ ∁ Q ]) where
+module _ (P⇒¬Q : ∀[ P ⇒ ∁ Q ]) where
 
-  Any⇒¬All : {xs : List# A R} → Any P xs → ¬ (All Q xs)
+  Any⇒¬All : Any P xs → ¬ (All Q xs)
   Any⇒¬All (here p)   (q ∷ _)  = P⇒¬Q p q
   Any⇒¬All (there ps) (_ ∷ qs) = Any⇒¬All ps qs
 
-  All⇒¬Any : {xs : List# A R} → All P xs → ¬ (Any Q xs)
+  All⇒¬Any : All P xs → ¬ (Any Q xs)
   All⇒¬Any (p ∷ _)  (here q)   = P⇒¬Q p q
   All⇒¬Any (_ ∷ ps) (there qs) = All⇒¬Any ps qs
 
-module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
+module _ (P? : Decidable P) where
 
-  ¬All⇒Any : {xs : List# A R} → ¬ (All P xs) → Any (∁ P) xs
+  ¬All⇒Any : ¬ (All P xs) → Any (∁ P) xs
   ¬All⇒Any {xs = []}      ¬ps = contradiction [] ¬ps
   ¬All⇒Any {xs = x ∷# xs} ¬ps with P? x
   ... |  true because  [p] = there (¬All⇒Any (¬ps ∘′ (invert [p] ∷_)))
   ... | false because [¬p] = here (invert [¬p])
 
-  ¬Any⇒All : {xs : List# A R} → ¬ (Any P xs) → All (∁ P) xs
+  ¬Any⇒All : ¬ (Any P xs) → All (∁ P) xs
   ¬Any⇒All {xs = []}      ¬ps = []
   ¬Any⇒All {xs = x ∷# xs} ¬ps with P? x
   ... |  true because  [p] = contradiction (here (invert [p])) ¬ps
@@ -69,30 +72,23 @@ module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where
 ------------------------------------------------------------------------
 -- remove
 
-module _ {R : Rel A r} {P : Pred A p} where
-
-  length-remove : {xs : List# A R} (k : Any P xs) →
-    length xs ≡ suc (length (xs ─ k))
-  length-remove (here _)  = refl
-  length-remove (there p) = cong suc (length-remove p)
+length-remove : (k : Any P xs) → length xs ≡ suc (length (xs ─ k))
+length-remove (here _)  = refl
+length-remove (there p) = cong suc (length-remove p)
 
 ------------------------------------------------------------------------
 -- append
 
-module _ {R : Rel A r} {P : Pred A p} where
-
-  append⁺ˡ : {xs ys : List# A R} {ps : All (_# ys) xs} →
-             Any P xs → Any P (append xs ys ps)
-  append⁺ˡ (here px) = here px
-  append⁺ˡ (there p) = there (append⁺ˡ p)
+append⁺ˡ : {ps : All (_# ys) xs} → Any P xs → Any P (append xs ys ps)
+append⁺ˡ (here px) = here px
+append⁺ˡ (there p) = there (append⁺ˡ p)
 
-  append⁺ʳ : {xs ys : List# A R} {ps : All (_# ys) xs} →
-             Any P ys → Any P (append xs ys ps)
-  append⁺ʳ {xs = []}      p = p
-  append⁺ʳ {xs = x ∷# xs} p = there (append⁺ʳ p)
+append⁺ʳ : {ps : All (_# ys) xs} → Any P ys → Any P (append xs ys ps)
+append⁺ʳ {xs = []}      p = p
+append⁺ʳ {xs = x ∷# xs} p = there (append⁺ʳ p)
 
-  append⁻ : ∀ xs {ys : List# A R} {ps : All (_# ys) xs} →
-            Any P (append xs ys ps) → Any P xs ⊎ Any P ys
-  append⁻ []        p         = inj₂ p
-  append⁻ (x ∷# xs) (here px) = inj₁ (here px)
-  append⁻ (x ∷# xs) (there p) = Sum.map₁ there (append⁻ xs p)
+append⁻ : ∀ xs {ps : All (_# ys) xs} →
+          Any P (append xs ys ps) → Any P xs ⊎ Any P ys
+append⁻ []        p         = inj₂ p
+append⁻ (x ∷# xs) (here px) = inj₁ (here px)
+append⁻ (x ∷# xs) (there p) = Sum.map₁ there (append⁻ xs p)

From d1d7a7ccade1f32bf380dc995b904856f88c2418 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jan 2026 12:24:37 +0000
Subject: [PATCH 12/13] fix: quantifier prefix

---
 src/Data/List/Fresh/Relation/Unary/Any/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
index d60073f426..c3c045f9a5 100644
--- a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
@@ -87,7 +87,7 @@ append⁺ʳ : {ps : All (_# ys) xs} → Any P ys → Any P (append xs ys ps)
 append⁺ʳ {xs = []}      p = p
 append⁺ʳ {xs = x ∷# xs} p = there (append⁺ʳ p)
 
-append⁻ : ∀ xs {ps : All (_# ys) xs} →
+append⁻ : ∀ xs {ys} {ps : All {R = R} (_# ys) xs} →
           Any P (append xs ys ps) → Any P xs ⊎ Any P ys
 append⁻ []        p         = inj₂ p
 append⁻ (x ∷# xs) (here px) = inj₁ (here px)

From ab384a4b1038ad841766fc2eab24ded360379422 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 28 Jan 2026 12:32:06 +0000
Subject: [PATCH 13/13] final tweaks

---
 src/Data/List/Fresh.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda
index 9d9d2bf594..805b0daddd 100644
--- a/src/Data/List/Fresh.agda
+++ b/src/Data/List/Fresh.agda
@@ -23,10 +23,10 @@ open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘′_; flip; id; _on_)
 open import Relation.Nullary using (does)
-open import Relation.Unary as Unary using (Pred; Decidable)
+open import Relation.Unary as Unary using (Pred)
 open import Relation.Binary.Core using (Rel; REL)
 open import Relation.Binary.Definitions as Binary using (Reflexive)
-open import Relation.Nary using (_⇒_; ∀[_])
+open import Relation.Nary using (_⇒_; ∀[_]; Decidable)
 
 
 private
@@ -45,7 +45,7 @@ private
 -- If we pick an R such that (R a b) means that a is different from b
 -- then we have a list of distinct values.
 
-module _ {a} (A : Set a) (R : Rel A r) where
+module _ (A : Set a) (R : Rel A r) where
 
   data List# : Set (a ⊔ r)
   fresh : REL A List# r
@@ -123,7 +123,7 @@ fromMaybe (just x) = [ x ]
 module _ (refl : Reflexive {A = A} R) where
 
   replicate   : ℕ → A → List# A R
-  replicate-# : (n : ℕ) (x : A) → x # replicate n x
+  replicate-# : ∀ n x → x # replicate n x
 
   replicate zero    x = []
   replicate (suc n) x = cons x (replicate n x) (replicate-# n x)