diff --git a/src/Maps.lagda b/src/Maps.lagda
index b0f1afd9..d76cb636 100644
--- a/src/Maps.lagda
+++ b/src/Maps.lagda
@@ -292,21 +292,22 @@ updates.
   update-permute′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
                    → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
   update-permute′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
+  ... | yes refl | yes refl  =  ⊥-elim (x≢y refl)
+  ... | no  x≢z  | yes refl  =  sym (update-eq′ ρ z w)
+  ... | yes refl | no  y≢z   =  update-eq′ ρ z v
+  ... | no  x≢z  | no  y≢z   =  trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))  
+\end{code}
+
+And a slightly different version of the same proof.
+
+\begin{code}  
+  update-permute′′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
+                   → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
+  update-permute′′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
   ... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
-  ... | no  x≢z | yes y≡z rewrite y≡z = {! sym (update-eq′ ρ z w)!}  
-  ... | yes x≡z | no  y≢z rewrite x≡z = {! update-eq′ ρ z v!}  
-  ... | no  x≢z | no  y≢z = {! trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z))!}
-
-{-
-Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them?
-Why does "λ y₁" appear in the final hole?
-
-?0 : w ≡ ((ρ , z ↦ w) z | z ≟ z)
-?1 : ((ρ , z ↦ v) z | z ≟ z) ≡ v
-?2 : (((λ y₁ → (ρ , x ↦ v) y₁ | x ≟ y₁) , y ↦ w) z | no y≢z) ≡
-(((λ y₁ → (ρ , y ↦ w) y₁ | y ≟ y₁) , x ↦ v) z | no x≢z)
-
--}
+  ... | no  x≢z | yes y≡z rewrite y≡z  =  sym (update-eq′ ρ z w)  
+  ... | yes x≡z | no  y≢z rewrite x≡z  =  update-eq′ ρ z v
+  ... | no  x≢z | no  y≢z  =  trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))  
 \end{code}
 </div>