Frame in both sides of a conjunction.

theories/proofmode/class_instances.v

@@ -565,12 +565,14 @@ Global Instance make_and_true_r P : MakeAnd P True P.
 Proof. by rewrite /MakeAnd right_id. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. done. Qed.
-Global Instance frame_and_l p R P1 P2 Q Q' :
-  Frame p R P1 Q → MakeAnd Q P2 Q' → Frame p R (P1 ∧ P2) Q' | 9.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
-Global Instance frame_and_r p R P1 P2 Q Q' :
-  Frame p R P2 Q → MakeAnd P1 Q Q' → Frame p R (P1 ∧ P2) Q' | 10.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+
+Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
+  MaybeFrame p R P1 Q1 progress1 →
+  MaybeFrame p R P2 Q2 progress2 →
+  TCEq (progress1 || progress2) true →
+  MakeAnd Q1 Q2 Q' →
+  Frame p R (P1 ∧ P2) Q' | 9.
+Proof. rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-; eauto 10 with I. Qed.
 
 Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
 Global Instance make_or_true_l P : MakeOr True P True.

theories/tests/proofmode.v

@@ -102,7 +102,7 @@ Proof. iIntros "[H [? _]]". by iFrame. Qed.
 
 Lemma test_iFrame_pure (x y z : M) :
   ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
-Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
+Proof. iIntros (Hv) "Hxy". iFrame (Hv) "Hxy". Qed.
 
 Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
   □ P1 -∗ Q2 -∗ P2 -∗ (P1 ∗ P2 ∗ False ∨ P2) ∗ (Q1 ∨ Q2).