Commit 91cbff6b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files


parent 43ee9e86
......@@ -208,7 +208,7 @@ Proof.
apply impl_intro_l. rewrite left_absorb. auto.
Lemma exists_impl_forall {A} P (Ψ : A PROP) :
Lemma exist_impl_forall {A} P (Ψ : A PROP) :
(( x : A, Ψ x) P) x : A, Ψ x P.
apply equiv_spec; split.
Supports Markdown
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