Commit 191a6f43 authored by Ralf Jung's avatar Ralf Jung

fix nits

parent 6d15cf39
......@@ -534,15 +534,14 @@ Proof.
Qed.
Section wandM.
Import proofmode.base.
Lemma test_wandM mP Q R :
(mP -? Q) - (Q - R) - (mP -? R).
Proof.
iIntros "HPQ HQR HP". Show.
iApply "HQR". iApply "HPQ". Show.
done.
Qed.
Import proofmode.base.
Lemma test_wandM mP Q R :
(mP -? Q) - (Q - R) - (mP -? R).
Proof.
iIntros "HPQ HQR HP". Show.
iApply "HQR". iApply "HPQ". Show.
done.
Qed.
End wandM.
End tests.
......
......@@ -23,8 +23,8 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
Section telescope_quantifiers.
Context {PROP : bi} {TT : tele}.
Lemma bi_tforall_forall (Ψ : TT -> PROP) :
(bi_tforall Ψ) (bi_forall Ψ).
Lemma bi_tforall_forall (Ψ : TT PROP) :
bi_tforall Ψ bi_forall Ψ.
Proof.
symmetry. unfold bi_tforall. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
......@@ -36,11 +36,11 @@ Section telescope_quantifiers.
by rewrite (forall_elim (TargS a p)).
+ move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
setoid_rewrite <- IH.
do 2 rewrite forall_elim. done.
rewrite 2!forall_elim. done.
Qed.
Lemma bi_texist_exist (Ψ : TT -> PROP) :
(bi_texist Ψ) (bi_exist Ψ).
Lemma bi_texist_exist (Ψ : TT PROP) :
bi_texist Ψ bi_exist Ψ.
Proof.
symmetry. unfold bi_texist. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
......
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