diff --git a/algebra/upred.v b/algebra/upred.v index 1958f06d7f6a1cf0dd2b7085ff2d4ca837846049..73d521139463509343e82842df645fa8ad66e1e9 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -980,7 +980,7 @@ Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, Proof. unseal; by split=> -[|n] x. Qed. Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊢ (▷ ∃ a, Φ a). Proof. unseal; by split=> -[|[|n]] x. Qed. -Lemma later_exist' `{Inhabited A} (Φ : A → uPred M) : (▷ ∃ a, Φ a) ⊢ ∃ a, ▷ Φ a. +Lemma later_exist_2 `{Inhabited A} (Φ : A → uPred M) : (▷ ∃ a, Φ a) ⊢ ∃ a, ▷ Φ a. Proof. unseal; split=> -[|[|n]] x; done || by exists inhabitant. Qed. Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ ▷ P ★ ▷ Q. Proof. @@ -1009,7 +1009,7 @@ Proof. Qed. Lemma later_exist `{Inhabited A} (Φ : A → uPred M) : ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a). -Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed. +Proof. apply: anti_symm; eauto using later_exist_2, later_exist_1. Qed. Lemma later_wand P Q : ▷ (P -★ Q) ⊢ ▷ P -★ ▷ Q. Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed. Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.