diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 4259b5f11b6490e5bb5575e0390e02874a4ce26b..9b494709ea5c51ade89e00314b54a58cd9d54ecc 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -724,4 +724,4 @@ Section gmultiset.
 End gmultiset.
 End big_op.
 
-Hint Resolve big_sepL_nil' big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.
+Hint Resolve big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 310281cf127cb13b93c6f51475711765c2443451..b4c84cda7e22812b3910d6b780ff20ba3d645059 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -343,14 +343,6 @@ Global Instance from_sep_bupd P Q1 Q2 :
   FromAnd false P Q1 Q2 → FromAnd false (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromAnd=><-. apply bupd_sep. Qed.
 
-Global Instance from_and_big_sepL_cons {A} (Φ : nat → A → uPred M) x l :
-  FromAnd false ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
-Proof. by rewrite /FromAnd big_sepL_cons. Qed.
-Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → uPred M) x l :
-  PersistentP (Φ 0 x) →
-  FromAnd true ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
-Proof. intros. by rewrite /FromAnd big_opL_cons always_and_sep_l. Qed.
-
 Global Instance from_and_big_sepL_app {A} (Φ : nat → A → uPred M) l1 l2 :
   FromAnd false ([∗ list] k ↦ y ∈ l1 ++ l2, Φ k y)
     ([∗ list] k ↦ y ∈ l1, Φ k y) ([∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y).
@@ -431,14 +423,8 @@ Global Instance into_and_laterN n p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p (▷^n P) (▷^n Q1) (▷^n Q2).
 Proof. rewrite /IntoAnd=>->. destruct p; by rewrite ?laterN_and ?laterN_sep. Qed.
 
-(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
-[frame_big_sepL_app] cannot be applied repeatedly often when having
-[ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
-Global Instance into_and_big_sepL_cons {A} p (Φ : nat → A → uPred M) l x l' :
-  IsCons l x l' →
-  IntoAnd p ([∗ list] k ↦ y ∈ l, Φ k y)
-    (Φ 0 x) ([∗ list] k ↦ y ∈ l', Φ (S k) y).
-Proof. rewrite /IsCons=>->. apply mk_into_and_sep. by rewrite big_sepL_cons. Qed.
+(* We use [IsApp] to make sure that [frame_big_sepL_app] cannot be applied
+repeatedly often when having [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
 Global Instance into_and_big_sepL_app {A} p (Φ : nat → A → uPred M) l l1 l2 :
   IsApp l l1 l2 →
   IntoAnd p ([∗ list] k ↦ y ∈ l, Φ k y)
@@ -473,11 +459,6 @@ Global Instance frame_sep_r p R P1 P2 Q Q' :
   Frame p R P2 Q → MakeSep P1 Q Q' → Frame p R (P1 ∗ P2) Q' | 10.
 Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc -(comm _ P1) assoc. Qed.
 
-Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → uPred M) R Q l x l' :
-  IsCons l x l' →
-  Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
-Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
 Global Instance frame_big_sepL_app {A} p (Φ : nat → A → uPred M) R Q l l1 l2 :
   IsApp l l1 l2 →
   Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗