diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v index 724ffb34ae11b373ac8cb6e1fbf77a669bd83f16..1127e290b4b9f33db6276c7f74b8d6b877c800b8 100644 --- a/theories/bi/derived_laws_bi.v +++ b/theories/bi/derived_laws_bi.v @@ -427,6 +427,15 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. Lemma sep_forall_r {A} (Φ : A → PROP) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q. Proof. by apply forall_intro=> a; rewrite forall_elim. Qed. +Lemma exist_wand_forall {A} P (Ψ : A → PROP) : + ((∃ x : A, Ψ x) -∗ P) ⊣⊢ ∀ x : A, Ψ x -∗ P. +Proof. + apply equiv_spec; split. + - apply forall_intro=>x. by rewrite -exist_intro. + - apply wand_intro_r, wand_elim_r', exist_elim=>x. + apply wand_intro_r. by rewrite (forall_elim x) wand_elim_r. +Qed. + Global Instance wand_iff_ne : NonExpansive2 (@bi_wand_iff PROP). Proof. solve_proper. Qed. Global Instance wand_iff_proper :