diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 4b7ccddc94eefd8fa5ac8d0690e9d3a312bd1689..010a153ecc95a8c6a57e395ef7b259882ea04b64 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1561,7 +1561,13 @@ Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
-(* Discrete instances *)
+Lemma later_bare_1 `{!Timeless (emp%I : PROP)} P : ▷ ■ P ⊢ ◇ ■ ▷ P.
+Proof.
+  rewrite /bi_bare later_and (timeless emp%I) except_0_and.
+  by apply and_mono, except_0_intro.
+Qed.
+
+(* Timeless instances *)
 Global Instance Timeless_proper : Proper ((≡) ==> iff) (@Timeless PROP).
 Proof. solve_proper. Qed.
 
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c5888cbb491584d2977723a5f78c24776b538af6..6934723128eeda77fbd8cb19c10a1ea7b42b06ff 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -353,9 +353,12 @@ Qed.
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
-Global Instance into_sep_bare `{PositiveBI PROP} P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep (■ P) (■ Q1) (■ Q2).
-Proof. rewrite /IntoSep /= => ->. by rewrite bare_sep. Qed.
+(* FIXME: This instance is kind of strange, it just gets rid of the â– . Also, it
+overlaps with `into_sep_bare_later`, and hence has lower precedence. *)
+Global Instance into_sep_bare P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (■ P) Q1 Q2 | 20.
+Proof. rewrite /IntoSep /= => ->. by rewrite bare_elim. Qed.
+
 Global Instance into_sep_persistently `{PositiveBI PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (□ P) (□ Q1) (□ Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
@@ -761,6 +764,17 @@ Global Instance into_sep_except_0 P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (◇ P) (◇ Q1) (◇ Q2).
 Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
 
+(* FIXME: This instance is overly specific, generalize it. *)
+Global Instance into_sep_bare_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
+  Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 → IntoSep (■ ▷ P) (■ ▷ Q1) (■ ▷ Q2).
+Proof.
+  rewrite /IntoSep /= => ?? ->.
+  rewrite -{1}(affine_bare Q1) -{1}(affine_bare Q2) later_sep !later_bare_1.
+  rewrite -except_0_sep /bi_except_0 bare_or. apply or_elim, bare_elim.
+  rewrite -(idemp bi_and (â–  â–· False)%I) persistent_and_sep_1.
+  by rewrite -(False_elim Q1) -(False_elim Q2).
+Qed.
+
 (* FromOr *)
 Global Instance from_or_later P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr (▷ P) (▷ Q1) (▷ Q2).