diff --git a/CHANGELOG.md b/CHANGELOG.md
index 43ca289cd733bf6ff232033597d4019135967efe..5b8d421ea3242d25925eb34845f2d49949a5fdfd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -30,6 +30,13 @@ API-breaking change is listed.
 - Add `Countable` instance for decidable Sigma types. (by Simon Gregersen)
 - Add tactics `compute_done` and `compute_by` for solving goals by computation.
 - Add `Inj` instances for `fmap` on option and maps.
+- Various changes to `Permutation` lemmas:
+  + Rename `Permutation_nil` → `Permutation_nil_r` and
+    and `Permutation_singleton` → `Permutation_singleton_r`.
+  + Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
+  + Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`.
+  + Add lemma `Permutation_cross_split`.
+  + Make lemma `elem_of_Permutation` a biimplication
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -37,6 +44,9 @@ The following `sed` script should perform most of the renaming
 sed -i -E '
 s/\bdecide_left\b/decide_True_pi/g
 s/\bdecide_right\b/decide_False_pi/g
+# Permutation
+s/\bPermutation_nil\b/Permutation_nil_r/g
+s/\bPermutation_singleton\b/Permutation_singleton_r/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 45a0cc67c8a0ec769052f38eb5f7f1a83cfda162..1d1dd5ca962655cecec59d12a6e8344728039218 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -938,7 +938,7 @@ Qed.
 Lemma map_to_list_singleton {A} i (x : A) :
   map_to_list ({[i:=x]} : M A) = [(i,x)].
 Proof.
-  apply Permutation_singleton. unfold singletonM, map_singleton.
+  apply Permutation_singleton_r. unfold singletonM, map_singleton.
   by rewrite map_to_list_insert, map_to_list_empty by eauto using lookup_empty.
 Qed.
 Lemma map_to_list_delete {A} (m : M A) i x :
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 21b71cc63eb923230b0ba956f20b074476529bbf..a458157121d40b54685db6761521bf9d3c5690f3 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -85,7 +85,7 @@ Qed.
 Lemma elements_empty' X : elements X = [] ↔ X ≡ ∅.
 Proof.
   split; intros HX; [by apply elements_empty_inv|].
-  by rewrite <-Permutation_nil, HX, elements_empty.
+  by rewrite <-Permutation_nil_r, HX, elements_empty.
 Qed.
 
 Lemma elements_union_singleton (X : C) x :
@@ -99,7 +99,7 @@ Proof.
 Qed.
 Lemma elements_singleton x : elements ({[ x ]} : C) = [x].
 Proof.
-  apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
+  apply Permutation_singleton_r. by rewrite <-(right_id ∅ (∪) {[x]}),
     elements_union_singleton, elements_empty by set_solver.
 Qed.
 Lemma elements_disj_union (X Y : C) :
diff --git a/theories/list.v b/theories/list.v
index f2d9a5d0e24c369635c4313a663f8b9d54257e32..1f8f5ed0ffd8af0cc37c93ff3bc5b41ba7e4b5b9 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -31,7 +31,6 @@ Global Instance: Params (@drop) 1 := {}.
 
 Global Arguments Permutation {_} _ _ : assert.
 Global Arguments Forall_cons {_} _ _ _ _ _ : assert.
-Global Remove Hints Permutation_cons : typeclass_instances.
 
 Notation "(::)" := cons (only parsing) : list_scope.
 Notation "( x ::.)" := (cons x) (only parsing) : list_scope.
@@ -1693,10 +1692,14 @@ Proof.
 Qed.
 
 (** ** Properties of the [Permutation] predicate *)
-Lemma Permutation_nil l : l ≡ₚ [] ↔ l = [].
+Lemma Permutation_nil_r l : l ≡ₚ [] ↔ l = [].
 Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
-Lemma Permutation_singleton l x : l ≡ₚ [x] ↔ l = [x].
+Lemma Permutation_singleton_r l x : l ≡ₚ [x] ↔ l = [x].
 Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
+Lemma Permutation_nil_l l : [] ≡ₚ l ↔ [] = l.
+Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_nil_r. Qed.
+Lemma Permutation_singleton_l l x : [x] ≡ₚ l ↔ [x] = l.
+Proof. by rewrite (symmetry_iff (≡ₚ)), Permutation_singleton_r. Qed.
 
 Lemma Permutation_skip x l l' : l ≡ₚ l' → x :: l ≡ₚ x :: l'.
 Proof. apply perm_skip. Qed.
@@ -1705,13 +1708,11 @@ Proof. apply perm_swap. Qed.
 Lemma Permutation_singleton_inj x y : [x] ≡ₚ [y] → x = y.
 Proof. apply Permutation_length_1. Qed.
 
-Global Instance Permutation_cons x : Proper ((≡ₚ) ==> (≡ₚ)) (@cons A x).
-Proof. by constructor. Qed.
-Global Existing Instance Permutation_app'.
-
-Global Instance elem_of_list_permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
+Global Instance length_Permutation_proper : Proper ((≡ₚ) ==> (=)) (@length A).
+Proof. induction 1; simpl; auto with lia. Qed.
+Global Instance elem_of_Permutation_proper x : Proper ((≡ₚ) ==> iff) (x ∈.).
 Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
-Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
+Global Instance NoDup_Permutation_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
 Proof.
   induction 1 as [|x l k Hlk IH | |].
   - by rewrite !NoDup_nil.
@@ -1720,23 +1721,28 @@ Proof.
   - intuition.
 Qed.
 
-Global Instance: Proper ((≡ₚ) ==> (=)) (@length A).
-Proof. induction 1; simpl; auto with lia. Qed.
-Global Instance: Comm (≡ₚ) (@app A).
+Global Instance app_Permutation_comm : Comm (≡ₚ) (@app A).
 Proof.
   intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
   - by rewrite (right_id_L [] (++)).
   - rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
 Qed.
-Global Instance: ∀ x : A, Inj (≡ₚ) (≡ₚ) (x ::.).
+
+Global Instance cons_Permutation_inj_r x : Inj (≡ₚ) (≡ₚ) (x ::.).
 Proof. red. eauto using Permutation_cons_inv. Qed.
-Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (k ++.).
+Global Instance app_Permutation_inj_r k : Inj (≡ₚ) (≡ₚ) (k ++.).
 Proof.
-  intros k. induction k as [|x k IH]; intros l1 l2; simpl; auto.
+  induction k as [|x k IH]; intros l1 l2; simpl; auto.
   intros. by apply IH, (inj (x ::.)).
 Qed.
-Global Instance: ∀ k : list A, Inj (≡ₚ) (≡ₚ) (.++ k).
-Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
+Global Instance cons_Permutation_inj_l k : Inj (=) (≡ₚ) (.:: k).
+Proof.
+  intros x1 x2 Hperm. apply Permutation_singleton_inj.
+  apply (inj (k ++.)). by rewrite !(comm (++) k).
+Qed.
+Global Instance app_Permutation_inj_l k : Inj (≡ₚ) (≡ₚ) (.++ k).
+Proof. intros l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
+
 Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
 Proof.
   intros Hl. apply replicate_as_elem_of. split.
@@ -1753,10 +1759,14 @@ Proof.
   revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
   by rewrite Permutation_swap, <-(IH i).
 Qed.
-Lemma elem_of_Permutation l x : x ∈ l → ∃ k, l ≡ₚ x :: k.
-Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.
+Lemma elem_of_Permutation l x : x ∈ l ↔ ∃ k, l ≡ₚ x :: k.
+Proof.
+  split.
+  - intros [i ?]%elem_of_list_lookup. eexists. by apply delete_Permutation.
+  - intros [k ->]. by left.
+Qed.
 
-Lemma Permutation_cons_inv l k x :
+Lemma Permutation_cons_inv_r l k x :
   k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
 Proof.
   intros Hk. assert (∃ i, k !! i = Some x) as [i Hi].
@@ -1766,6 +1776,30 @@ Proof.
   - rewrite <-delete_take_drop. apply (inj (x ::.)).
     by rewrite <-Hk, <-(delete_Permutation k) by done.
 Qed.
+Lemma Permutation_cons_inv_l l k x :
+  x :: l ≡ₚ k → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
+Proof. by intros ?%(symmetry_iff (≡ₚ))%Permutation_cons_inv_r. Qed.
+
+Lemma Permutation_cross_split l la lb lc ld :
+  la ++ lb ≡ₚ l →
+  lc ++ ld ≡ₚ l →
+  ∃ lac lad lbc lbd,
+    lac ++ lad ≡ₚ la ∧ lbc ++ lbd ≡ₚ lb ∧ lac ++ lbc ≡ₚ lc ∧ lad ++ lbd ≡ₚ ld.
+Proof.
+  intros <-. revert lc ld.
+  induction la as [|x la IH]; simpl; intros lc ld Hperm.
+  { exists [], [], lc, ld. by rewrite !(right_id_L [] (++)). }
+  assert (x ∈ lc ++ ld)
+    as [[lc' Hlc]%elem_of_Permutation|[ld' Hld]%elem_of_Permutation]%elem_of_app.
+  { rewrite Hperm, elem_of_cons. auto. }
+  - rewrite Hlc in Hperm. simpl in Hperm. apply (inj (x ::.)) in Hperm.
+    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
+    exists (x :: lac), lad, lbc, lbd; simpl. by rewrite Ha, Hb, Hc, Hd.
+  - rewrite Hld, <-Permutation_middle in Hperm. apply (inj (x ::.)) in Hperm.
+    apply IH in Hperm as (lac&lad&lbc&lbd&Ha&Hb&Hc&Hd).
+    exists lac, (x :: lad), lbc, lbd; simpl.
+    by rewrite <-Permutation_middle, Ha, Hb, Hc, Hd.
+Qed.
 
 Lemma Permutation_inj l1 l2 :
   Permutation l1 l2 ↔
@@ -1787,7 +1821,7 @@ Proof.
     induction l1 as [|x l1 IH]; intros l2 f Hlen Hf Hl; [by destruct l2|].
     rewrite (delete_Permutation l2 (f 0) x) by (by rewrite <-Hl).
     pose (g n := let m := f (S n) in if lt_eq_lt_dec m (f 0) then m else m - 1).
-    eapply Permutation_cons, (IH _ g).
+    apply Permutation_skip, (IH _ g).
     + rewrite length_delete by (rewrite <-Hl; eauto); simpl in *; lia.
     + unfold g. intros i j Hg.
       repeat destruct (lt_eq_lt_dec _ _) as [[?|?]|?]; simplify_eq/=; try lia.
diff --git a/theories/sorting.v b/theories/sorting.v
index 3f019e54d0e6902b2a0de8d23074b656831b0621..afd9da0b1ba3858477cf3fc3a7ccfa29d84353ae 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -77,7 +77,7 @@ Section sorted.
     intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
     { symmetry. by apply Permutation_nil. }
     destruct Hl2 as [|x2 l2 ? Hx2].
-    { by apply Permutation_nil in E. }
+    { by apply Permutation_nil_r in E. }
     assert (x1 = x2); subst.
     { rewrite Forall_forall in Hx1, Hx2.
       assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).