diff --git a/Analysis/Forward/Lattices.agda b/Analysis/Forward/Lattices.agda
index 3df50bf..9b28a5f 100644
--- a/Analysis/Forward/Lattices.agda
+++ b/Analysis/Forward/Lattices.agda
@@ -65,7 +65,7 @@ open IsLattice isLatticeᵛ
         ; ⊔-idemp to ⊔ᵛ-idemp
         )
     public
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L vars vars-Unique
+open VariableValuesFiniteMap.FixedHeight vars-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
@@ -93,8 +93,7 @@ open StateVariablesFiniteMap
         ; ≈-sym to ≈ᵐ-sym
         )
     public
-
-open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight State VariableValues states states-Unique
+open StateVariablesFiniteMap.FixedHeight states-Unique
     using ()
     renaming
         ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index 821c617..4692b89 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -281,7 +281,7 @@ Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v
 ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
         ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
 
-module IterProdIsomorphism where
+private module IterProdIsomorphism where
     open WithKeys
     open import Data.Unit using (tt)
     open import Lattice.Unit using ()
@@ -323,15 +323,12 @@ module IterProdIsomorphism where
         in
             (((k , v) ∷ fm' , push k≢fm' ufm') , kvs≡ks)
 
+    _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
+    _≈ⁱᵖ_ {n} = IP._≈_ {n}
 
-    private
-        _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
-        _≈ⁱᵖ_ {n} = IP._≈_ {n}
-
-        _⊔ⁱᵖ_ : ∀ {ks : List A} →
-                IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
-        _⊔ⁱᵖ_ {ks} = IP._⊔_ {length ks}
-
+    _⊔ⁱᵖ_ : ∀ {ks : List A} →
+            IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
+    _⊔ⁱᵖ_ {ks} = IP._⊔_ {length ks}
 
     to-build : ∀ {b : B} {ks : List A} (uks : Unique ks) →
                let fm = to uks (IP.build b tt (length ks))
@@ -615,7 +612,7 @@ module IterProdIsomorphism where
                         in
                             (v' , (v₁⊔v₂≈v' , there v'∈fm'))
 
-    module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} where
+    module FixedHeight {ks : List A} {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} (uks : Unique ks) where
         import Isomorphism
         open Isomorphism.TransportFiniteHeight
             (IP.isFiniteHeightLattice {k = length ks} {{fhB = fixedHeightᵘ}}) (isLattice ks)
@@ -635,3 +632,4 @@ module IterProdIsomorphism where
             to-build uks k v k,v∈⊥
 
 open WithKeys ks public
+module FixedHeight = IterProdIsomorphism.FixedHeight