diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index f3e5d9502ab5146563481ca229c9e6552bfd8ff5..954707291a272becef62d5ed866667391c925cd7 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -1181,6 +1181,9 @@ Proof. destruct p; simpl; auto using intuitionistically_sep. Qed.
 Lemma intuitionistically_if_idemp p P : □?p □?p P ⊣⊢ □?p P.
 Proof. destruct p; simpl; auto using intuitionistically_idemp. Qed.
 
+Lemma intuitionistically_if_unfold p P : □?p P ⊣⊢ <affine>?p <pers>?p P.
+Proof. by destruct p. Qed.
+
 (* Properties of persistent propositions *)
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
 Proof. solve_proper. Qed.
@@ -1288,6 +1291,8 @@ Global Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
 Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
 Global Instance affinely_affine P : Affine (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance affinely_if_affine p P : Affine P → Affine (<affine>?p P).
+Proof. destruct p; simpl; apply _. Qed.
 Global Instance intuitionistically_affine P : Affine (â–¡ P).
 Proof. rewrite /bi_intuitionistically. apply _. Qed.