diff --git a/tests/proofmode.v b/tests/proofmode.v index 9b57025be25c5d0442c990372913fc5341ef7ec9..d2ba302b5af08a316d72bbea00f762b3aef977cf 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -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. diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v index 554cd0b2733bc5deeea166c93390b65000c35cd7..d54533929a945c82d8872083527dacbaaff6251c 100644 --- a/theories/bi/telescopes.v +++ b/theories/bi/telescopes.v @@ -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 _).