diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 97a7004b32212b1189f548091699688fc8762f35..ec1f9845211074331ab225e4b52f96d037345260 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -667,6 +667,12 @@ Proof. intros. by rewrite /AndSplit always_and_sep_l. Qed.
 Global Instance and_split_sep_persistent_r P1 P2 :
   PersistentP P2 → AndSplit (P1 ★ P2) P1 P2.
 Proof. intros. by rewrite /AndSplit always_and_sep_r. Qed.
+Global Instance and_split_always P Q1 Q2 :
+  AndSplit P Q1 Q2 → AndSplit (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /AndSplit=> <-. by rewrite always_and. Qed.
+Global Instance and_split_later P Q1 Q2 :
+  AndSplit P Q1 Q2 → AndSplit (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /AndSplit=> <-. by rewrite later_and. Qed.
 
 Lemma tac_and_split Δ P Q1 Q2 : AndSplit P Q1 Q2 → (Δ ⊢ Q1) → (Δ ⊢ Q2) → Δ ⊢ P.
 Proof. intros. rewrite -(and_split P). by apply and_intro. Qed.
@@ -677,6 +683,13 @@ Arguments sep_split : clear implicits.
 
 Global Instance sep_split_sep P1 P2 : SepSplit (P1 ★ P2) P1 P2 | 100.
 Proof. done. Qed.
+Global Instance sep_split_always P Q1 Q2 :
+  SepSplit P Q1 Q2 → SepSplit (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /SepSplit=> <-. by rewrite always_sep. Qed.
+Global Instance sep_split_later P Q1 Q2 :
+  SepSplit P Q1 Q2 → SepSplit (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /SepSplit=> <-. by rewrite later_sep. Qed.
+
 Global Instance sep_split_ownM (a b : M) :
   SepSplit (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
 Proof. by rewrite /SepSplit ownM_op. Qed.