diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 3460e251b01b121f4281271df676ab6769455d13..0ed7413b42de027f6e0c5c3f8cdf26b15d10a182 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -75,6 +75,19 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   â–¡ P
   
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  l : list nat
+  P : PROP
+  ============================
+  "HP" : P
+  _ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
+  _ : <affine> ⌜x = x⌝ ∗ ([∗ list] y ∈ l, <affine> ⌜y = y⌝)
+  --------------------------------------∗
+  P
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 2359d047af444eab583506490496ecb30dd49121..1931f99ed7415bc2487e0d5505cf3e2df6ee248f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -485,6 +485,12 @@ Proof.
   iIntros "[??]". iSplit; last done. Show. done.
 Qed.
 
+Lemma test_big_sepL_simpl x (l : list nat) P :
+  P -∗
+  ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
+  ([∗ list] y ∈ x :: l, <affine> ⌜ y = y ⌝) -∗
+  P.
+Proof. iIntros "HP ?? /=". Show. done. Qed.
 End tests.
 
 (** Test specifically if certain things print correctly. *)
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 317ac0b316706dcce9bba9ad46399a41dfdc9e8c..f2fe3bd8e51d6798425ae34d1357eedad94011de 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -7,7 +7,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  "H" : inv N (<pers> P)%I
+  "H" : inv N (<pers> P)
   "H2" : â–· <pers> P
   --------------------------------------â–¡
   |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
@@ -21,7 +21,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  "H" : inv N (<pers> P)%I
+  "H" : inv N (<pers> P)
   "H2" : â–· <pers> P
   --------------------------------------â–¡
   "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
@@ -39,7 +39,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  _ : cinv N γ (<pers> P)%I
+  _ : cinv N γ (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown" : cinv_own γ p
@@ -57,7 +57,7 @@
   N : namespace
   P : iProp Σ
   ============================
-  _ : cinv N γ (<pers> P)%I
+  _ : cinv N γ (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown" : cinv_own γ p
@@ -77,7 +77,7 @@
   P : iProp Σ
   H2 : ↑N ⊆ E2
   ============================
-  _ : na_inv t N (<pers> P)%I
+  _ : na_inv t N (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown1" : na_own t E1
@@ -98,7 +98,7 @@
   P : iProp Σ
   H2 : ↑N ⊆ E2
   ============================
-  _ : na_inv t N (<pers> P)%I
+  _ : na_inv t N (<pers> P)
   "HP" : â–· <pers> P
   --------------------------------------â–¡
   "Hown1" : na_own t E1
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 33019f9c16a749ca117074f769ef5be58b6f4137..03fb2f02b03a781a6aef990515e3cb46956c3304 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -8,10 +8,10 @@ Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%I.
 
 Notation "" := Enil (only printing) : proof_scope.
-Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
+Notation "Γ H : P" := (Esnoc Γ (INamed H) P%I)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  '[' P ']' '//'", only printing) : proof_scope.
-Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
+Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P%I)
   (at level 1, P at level 200,
    left associativity, format "Γ '_'  :  '[' P ']' '//'", only printing) : proof_scope.