diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index fcb0367ffd20adfdbd08547fae4abc10cdd2b21e..26e043615bffcd9371be6017587d47d1d350de93 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -25,6 +25,7 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
   end.
 Instance: Params (@big_opL) 4.
 Arguments big_opL {M} o {_ A} _ !_ /.
+Typeclasses Opaque big_opL.
 Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
   (at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
    format "[^ o  list]  k ↦ x  ∈  l ,  P") : C_scope.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 43b745d9df2115d406dd9b0271ddc4ea6f78eb92..72b8e10d8b6f3d4dc7020536c5ace4c2023a8c0c 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -151,21 +151,21 @@ Section list.
 
   Global Instance big_sepL_nil_persistent Φ :
     PersistentP ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. apply _. Qed.
+  Proof. simpl; apply _. Qed.
   Global Instance big_sepL_persistent Φ l :
     (∀ k x, PersistentP (Φ k x)) → PersistentP ([∗ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
   Global Instance big_sepL_persistent_id Ps : PersistentL Ps → PersistentP ([∗] Ps).
-  Proof. induction 1; apply _. Qed.
+  Proof. induction 1; simpl; apply _. Qed.
 
   Global Instance big_sepL_nil_timeless Φ :
     TimelessP ([∗ list] k↦x ∈ [], Φ k x).
-  Proof. apply _. Qed.
+  Proof. simpl; apply _. Qed.
   Global Instance big_sepL_timeless Φ l :
     (∀ k x, TimelessP (Φ k x)) → TimelessP ([∗ list] k↦x ∈ l, Φ k x).
   Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
   Global Instance big_sepL_timeless_id Ps : TimelessL Ps → TimelessP ([∗] Ps).
-  Proof. induction 1; apply _. Qed.
+  Proof. induction 1; simpl; apply _. Qed.
 End list.
 
 Section list2.
@@ -589,4 +589,4 @@ Section gmultiset.
 End gmultiset.
 End big_op.
 
-Hint Resolve big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.
+Hint Resolve big_sepL_nil' 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 e24a45acf24cb3d1d882a59ba120507e21b5e9ab..b5176725dfeb0dcb969e69dd0e15d3f286140d1a 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -343,6 +343,14 @@ 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).
@@ -423,8 +431,14 @@ 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 [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. *)
+(* 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.
 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)
@@ -459,6 +473,11 @@ 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) ∗