diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index cf20a664ce56744448d7383205384cb70fe3b74e..f803dbd1061fce8c1b8dc19602a383dae4a27a56 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -53,7 +53,7 @@ Proof.
   - exact: persistently_idemp_2.
   - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
     trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
-    + apply forall_intro=>[[]].
+    + apply forall_intro=>-[].
     + etrans; first exact: persistently_forall_2.
       apply persistently_mono. exact: pure_intro.
   - (* ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q) (ADMISSIBLE) *)
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 9d29b036cbbcb0bec2099834d2b50dcda417127d..c7aa96c06cc7bbc2493856d0634c54c94a06df41 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -862,8 +862,7 @@ Lemma persistently_and P Q : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q.
 Proof. apply (anti_symm _); by auto using persistently_and_2. Qed.
 Lemma persistently_or P Q : <pers> (P ∨ Q) ⊣⊢ <pers> P ∨ <pers> Q.
 Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
-Lemma persistently_impl P Q :
-  <pers> (P → Q) ⊢ <pers> P → <pers> Q.
+Lemma persistently_impl P Q : <pers> (P → Q) ⊢ <pers> P → <pers> Q.
 Proof.
   apply impl_intro_l; rewrite -persistently_and.
   apply persistently_mono, impl_elim with P; auto.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index ef82d1380c51ab2e0c0e7d8e543874d441a5ffe2..3317c511c6bfc70a2dbc4ef288a4c7820da02266 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -107,7 +107,7 @@ Section bi_mixin.
     The null-ary case, [persistently_True : True ⊢ <pers> True], is derivable from the
     other laws. *)
     bi_mixin_persistently_and_2 (P Q : PROP) :
-      ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q);
+      (<pers> P) ∧ (<pers> Q) ⊢ <pers> (P ∧ Q);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
       <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);
 
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index 9b4c499aba043ea4b0f392d730b89d782fe7004f..0bc59a54f7abd01e3a877ccfae7679c8506292cb 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -26,7 +26,8 @@ Section core.
     by iApply "HPQ".
   Qed.
 
-  Global Instance coreP_persistent `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
+  Global Instance coreP_persistent
+      `{!BiPersistentlyForall PROP, !BiPersistentlyImplPlainly PROP} P :
     Persistent (coreP P).
   Proof.
     rewrite /coreP /Persistent. iIntros "HC" (Q).