Commit 4cf7fb98 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Lemma [exists_impl_forall] for currying an exists into a forall.

parent 302ffc56
......@@ -684,6 +684,15 @@ Proof.
- by apply impl_intro_l; rewrite left_id.
Lemma exists_impl_forall {A} P (Ψ : A uPred M) :
(( x : A, Ψ x) P) ⊣⊢ x : A, Ψ x P.
apply equiv_spec; split.
- apply forall_intro=>x. by rewrite -exist_intro.
- apply impl_intro_r, impl_elim_r', exist_elim=>x.
apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
Lemma or_and_l P Q R : P Q R ⊣⊢ (P Q) (P R).
apply (anti_symm ()); first auto.
......@@ -817,7 +826,7 @@ Proof.
intros P; unseal; split=> n x Hvalid; split.
- intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_mono, cmra_includedN_r.
- by intros ?; exists (core x), x; rewrite cmra_core_l.
Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
by intros P Q; unseal; split=> n x ?; split;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment