diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda
index cffc277..32bda52 100644
--- a/Lattice/FiniteValueMap.agda
+++ b/Lattice/FiniteValueMap.agda
@@ -312,25 +312,39 @@ module IterProdIsomorphism where
             fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
                                      (IP.≈-sym (length ks') rest₁≈rest₂)
 
-    from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → _≈ⁱᵖ_ {length ks} (from (fm₁ ⊔ᵐ fm₂)) (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
+    from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) →
+                  _≈ⁱᵖ_ {length ks} (from (fm₁ ⊔ᵐ fm₂))
+                                    (_⊔ⁱᵖ_ {ks} (from fm₁) (from fm₂))
     from-⊔-distr {[]} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
     from-⊔-distr {k ∷ ks} fm₁@(m₁ , _) fm₂@(m₂ , _)
-        with first-key-in-map (fm₁ ⊔ᵐ fm₂) | first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value (fm₁ ⊔ᵐ fm₂) | from-first-value fm₁ | from-first-value fm₂
+        with first-key-in-map (fm₁ ⊔ᵐ fm₂)
+          | first-key-in-map fm₁
+          | first-key-in-map fm₂
+          | from-first-value (fm₁ ⊔ᵐ fm₂)
+          | from-first-value fm₁ | from-first-value fm₂
     ...   | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
             with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
-    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂} k,v₂∈fm₂))
-    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁} k,v₁∈fm₁))
+    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂}
+                                                                k,v₂∈fm₂))
+    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁}
+                                                                k,v₁∈fm₁))
     ...       | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
                 rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
                 rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
                 rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂
                 rewrite from-rest (fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
                 = ( IsLattice.≈-refl lB
-                  , IsEquivalence.≈-trans (IP.≈-equiv (length ks)) (from-preserves-≈ {_} {pop (fm₁ ⊔ᵐ fm₂)} {pop fm₁ ⊔ᵐ pop fm₂} (pop-⊔-distr fm₁ fm₂)) ((from-⊔-distr (pop fm₁) (pop fm₂)))
+                  , IsEquivalence.≈-trans
+                        (IP.≈-equiv (length ks))
+                        (from-preserves-≈ {_} {pop (fm₁ ⊔ᵐ fm₂)}
+                                              {pop fm₁ ⊔ᵐ pop fm₂}
+                                              (pop-⊔-distr fm₁ fm₂))
+                        ((from-⊔-distr (pop fm₁) (pop fm₂)))
                   )
 
 
-    to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) → to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂)
+    to-⊔-distr : ∀ {ks : List A} (uks : Unique ks) → (ip₁ ip₂ : IterProd (length ks)) →
+                 to uks (_⊔ⁱᵖ_ {ks} ip₁ ip₂) ≈ᵐ (to uks ip₁ ⊔ᵐ to uks ip₂)
     to-⊔-distr {[]} empty tt tt = ((λ k v ()), (λ k v ()))
     to-⊔-distr {ks@(k ∷ ks')} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) = (fm⊆fm₁fm₂ , fm₁fm₂⊆fm)
         where
@@ -344,27 +358,45 @@ module IterProdIsomorphism where
             fm⊆fm₁fm₂ k v (here refl) =
                 (v₁ ⊔₂ v₂
                 , (IsLattice.≈-refl lB
-                  , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂} (here refl) (here refl)
+                  , ⊔-combines {k} {v₁} {v₂} {proj₁ fm₁} {proj₁ fm₂}
+                               (here refl) (here refl)
                   )
                 )
             fm⊆fm₁fm₂ k' v (there k',v∈fm')
                 with (fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂
-                with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂)) ← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
-                with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂))) ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
-                (v' , (v₁⊔v₂≈v' , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂} (there v₁∈fm'₁) (there v₂∈fm'₂)))
+                with (v' , (v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂))
+                     ← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
+                with (_ , (refl , (v₁∈fm'₁ , v₂∈fm'₂)))
+                     ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
+                ( v'
+                , ( v₁⊔v₂≈v'
+                  , ⊔-combines {m₁ = proj₁ fm₁} {m₂ = proj₁ fm₂}
+                               (there v₁∈fm'₁) (there v₂∈fm'₂)
+                  )
+                )
 
             fm₁fm₂⊆fm : (fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm
             fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
-                with (_ , fm'₁fm'₂⊆fm') ← to-⊔-distr uks' rest₁ rest₂
-                with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂))) ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
+                with (_ , fm'₁fm'₂⊆fm')
+                     ← to-⊔-distr uks' rest₁ rest₂
+                with (_ , (refl , (v₁∈fm₁ , v₂∈fm₂)))
+                     ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
                 with v₁∈fm₁ | v₂∈fm₂
-            ...   | here refl | here refl = (v , (IsLattice.≈-refl lB , here refl))
-            ...   | here refl | there k',v₂∈fm₂' = ⊥-elim (All¬-¬Any k≢ks' (subst (λ list → k' ∈ˡ list) (proj₂ fm₂') (forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
-            ...   | there k',v₁∈fm₁' | here refl = ⊥-elim (All¬-¬Any k≢ks' (subst (λ list → k' ∈ˡ list) (proj₂ fm₁') (forget {m = proj₁ fm₁'} k',v₁∈fm₁')))
+            ...   | here refl | here refl =
+                    (v , (IsLattice.≈-refl lB , here refl))
+            ...   | here refl | there k',v₂∈fm₂' =
+                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
+                                                   (forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
+            ...   | there k',v₁∈fm₁' | here refl =
+                    ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
+                                                   (forget {m = proj₁ fm₁'} k',v₁∈fm₁')))
             ...   | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
                         let
-                            k',v₁v₂∈fm₁'fm₂' = ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'} k',v₁∈fm₁' k',v₂∈fm₂'
-                            (v' , (v₁⊔v₂≈v' , v'∈fm')) = fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
+                            k',v₁v₂∈fm₁'fm₂' =
+                                ⊔-combines {m₁ = proj₁ fm₁'} {m₂ = proj₁ fm₂'}
+                                           k',v₁∈fm₁' k',v₂∈fm₂'
+                            (v' , (v₁⊔v₂≈v' , v'∈fm')) =
+                                fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
                         in
                             (v' , (v₁⊔v₂≈v' , there v'∈fm'))