diff --git a/tests/proofmode.v b/tests/proofmode.v
index 485d249c6cc82948d9d0e952290752d257fd61ec..28d3d010d1c9c466b54035267e9b0325ef421f63 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -455,6 +455,13 @@ Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.
 
+Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
+  P -∗ <affine> Q -∗ <affine> (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
+  P -∗ Q -∗ <affine> (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index ff71e3a1001b27ead954bfde8e6bbe3c52d12cf1..6d4a660ed5eddbca2ed38af982b8677bc4b6cc63 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -204,11 +204,12 @@ Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_em
 Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
 Proof. by rewrite /MakeAffinely. Qed.
 
-Global Instance frame_affinely R P Q Q' :
-  Frame true R P Q → MakeAffinely Q Q' → Frame true R (<affine> P) Q'.
+Global Instance frame_affinely p R P Q Q' :
+  TCOr (TCEq p true) (Affine R) →
+  Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'.
 Proof.
-  rewrite /Frame /MakeAffinely=> <- <- /=.
-  rewrite -{1}(affine_affinely (â–¡ R)%I) affinely_sep_2 //.
+  rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
+    by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2.
 Qed.
 
 Global Instance make_intuitionistically_emp :