diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index aaebdd5bb2..7ac00bac5b 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -243,12 +243,9 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
 ++-comm : Commutative {A = List A} _↭_ _++_
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
 ++-comm (x ∷ xs) ys = begin
-  x ∷ xs ++ ys         ↭⟨ prep x (++-comm xs ys) ⟩
-  x ∷ ys ++ xs         ≡⟨ cong (λ v → x ∷ v ++ xs) (≡.sym (Lₚ.++-identityʳ _)) ⟩
-  (x ∷ ys ++ []) ++ xs ↭⟨ ++⁺ʳ xs (↭-sym (shift x ys [])) ⟩
-  (ys ++ [ x ]) ++ xs  ↭⟨ ++-assoc ys [ x ] xs ⟩
-  ys ++ ([ x ] ++ xs)  ≡⟨⟩
-  ys ++ (x ∷ xs)       ∎
+  x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
+  x ∷ ys ++ xs   ↭˘⟨ shift x ys xs ⟩
+  ys ++ (x ∷ xs) ∎
 
 ++-isMagma : IsMagma {A = List A} _↭_ _++_
 ++-isMagma = record
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 025a3a124c..08f1b35dc2 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -197,12 +197,9 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
 ++-comm : Commutative _↭_ _++_
 ++-comm []       ys = ↭-sym (++-identityʳ ys)
 ++-comm (x ∷ xs) ys = begin
-  x ∷ xs ++ ys         <⟨ ++-comm xs ys ⟩
-  x ∷ ys ++ xs         ≡⟨ cong (λ v → x ∷ v ++ xs) (≡.sym (Lₚ.++-identityʳ _)) ⟩
-  (x ∷ ys ++ []) ++ xs ↭⟨ ++⁺ʳ xs (↭-sym (↭-shift ys [])) ⟩
-  (ys ++ [ x ]) ++ xs  ↭⟨ ++-assoc ys [ x ] xs ⟩
-  ys ++ ([ x ] ++ xs)  ≡⟨⟩
-  ys ++ (x ∷ xs)       ∎
+  x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
+  x ∷ ys ++ xs   ↭˘⟨ ↭-shift ys xs ⟩
+  ys ++ (x ∷ xs) ∎
 
 -- Structures