From ee12aa643d208db5cce8e600e9a7a1eee9fa1023 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 19 Mar 2018 16:22:38 +0100
Subject: [PATCH] rename affinely_persistently -> intuitionistically; and make
 it a TC-opaque definition

---
 theories/base_logic/base_logic.v              |   2 +-
 theories/base_logic/derived.v                 |   6 +-
 .../base_logic/lib/fancy_updates_from_vs.v    |   2 +-
 theories/bi/big_op.v                          |  12 +-
 theories/bi/derived_connectives.v             |  20 +-
 theories/bi/derived_laws.v                    | 226 +++++++++++-------
 theories/bi/embedding.v                       |   4 +
 theories/bi/fixpoint.v                        |   3 +-
 theories/bi/lib/fractional.v                  |   2 +-
 theories/bi/monpred.v                         |   4 +
 theories/bi/plainly.v                         |  14 +-
 theories/heap_lang/lib/increment.v            |   2 +-
 theories/proofmode/class_instances.v          | 161 +++++++------
 theories/proofmode/coq_tactics.v              | 137 ++++++-----
 theories/proofmode/modalities.v               |  40 ++--
 theories/proofmode/modality_instances.v       |  14 +-
 theories/proofmode/monpred.v                  |   8 +-
 theories/proofmode/tactics.v                  |   1 +
 theories/tests/proofmode_monpred.v            |   1 -
 19 files changed, 377 insertions(+), 282 deletions(-)

diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 4aecb160d..edcc029b4 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -73,7 +73,7 @@ Qed.
 Global Instance into_and_ownM p (a b1 b2 : M) :
   IsOp a b1 b2 â†’ IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof.
-  intros. apply affinely_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
+  intros. apply intuitionistically_if_mono. by rewrite (is_op a) ownM_op sep_and.
 Qed.
 
 Global Instance into_sep_ownM (a b1 b2 : M) :
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 2bbd331ba..2f4352e1d 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -20,7 +20,8 @@ Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : âœ“ a âŠ¢ <pers> (âœ“ a :
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
 Lemma affinely_persistently_ownM (a : M) : CoreId a â†’ â–¡ uPred_ownM a âŠ£âŠ¢ uPred_ownM a.
 Proof.
-  rewrite affine_affinely=>?; apply (anti_symm _); [by rewrite persistently_elim|].
+  rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
+    [by rewrite persistently_elim|].
   by rewrite {1}persistently_ownM_core core_id_core.
 Qed.
 Lemma ownM_invalid (a : M) : Â¬ âœ“{0} a â†’ uPred_ownM a âŠ¢ False.
@@ -33,7 +34,8 @@ Lemma plainly_cmra_valid {A : cmraT} (a : A) : â–  âœ“ a âŠ£âŠ¢ âœ“ a.
 Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
 Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : â–¡ âœ“ a âŠ£âŠ¢ âœ“ a.
 Proof.
-  rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
+  rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
+    first by rewrite persistently_elim.
   apply:persistently_cmra_valid_1.
 Qed.
 Lemma bupd_ownM_update x y : x ~~> y â†’ uPred_ownM x âŠ¢ |==> uPred_ownM y.
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index f8e87f2f8..b47fa0df6 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -68,4 +68,4 @@ Proof.
   iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
   iExists (R âˆ— Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
 Qed.
-End fupd.
\ No newline at end of file
+End fupd.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index a51063fdc..dc04b291a 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -150,10 +150,10 @@ Section sep_list.
   Proof.
     apply wand_intro_l. revert Î¦ Î¨. induction l as [|x l IH]=> Î¦ Î¨ /=.
     { by rewrite sep_elim_r. }
-    rewrite affinely_persistently_sep_dup -assoc [(â–¡ _ âˆ— _)%I]comm -!assoc assoc.
+    rewrite intuitionistically_sep_dup -assoc [(â–¡ _ âˆ— _)%I]comm -!assoc assoc.
     apply sep_mono.
     - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
-      by rewrite affinely_persistently_elim wand_elim_l.
+      by rewrite intuitionistically_elim wand_elim_l.
     - rewrite comm -(IH (Î¦ âˆ˜ S) (Î¨ âˆ˜ S)) /=.
       apply sep_mono_l, affinely_mono, persistently_mono.
       apply forall_intro=> k. by rewrite (forall_elim (S k)).
@@ -423,10 +423,10 @@ Section gmap.
   Proof.
     apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
     { by rewrite sep_elim_r. }
-    rewrite !big_sepM_insert // affinely_persistently_sep_dup.
+    rewrite !big_sepM_insert // intuitionistically_sep_dup.
     rewrite -assoc [(â–¡ _ âˆ— _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
-      by rewrite True_impl affinely_persistently_elim wand_elim_l.
+      by rewrite True_impl intuitionistically_elim wand_elim_l.
     - rewrite comm -IH /=.
       apply sep_mono_l, affinely_mono, persistently_mono, forall_mono=> k.
       apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
@@ -584,10 +584,10 @@ Section gset.
   Proof.
     apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
     { by rewrite sep_elim_r. }
-    rewrite !big_sepS_insert // affinely_persistently_sep_dup.
+    rewrite !big_sepS_insert // intuitionistically_sep_dup.
     rewrite -assoc [(â–¡ _ âˆ— _)%I]comm -!assoc assoc. apply sep_mono.
     - rewrite (forall_elim x) pure_True; last set_solver.
-      by rewrite True_impl affinely_persistently_elim wand_elim_l.
+      by rewrite True_impl intuitionistically_elim wand_elim_l.
     - rewrite comm -IH /=. apply sep_mono_l, affinely_mono, persistently_mono.
       apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
       by rewrite pure_True ?True_impl; last set_solver.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index a381402bf..5857b235e 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -26,9 +26,6 @@ Typeclasses Opaque bi_affinely.
 Notation "'<affine>' P" := (bi_affinely P)
   (at level 20, right associativity) : bi_scope.
 
-Notation "â–¡ P" := (<affine> <pers> P)%I
-  (at level 20, right associativity) : bi_scope.
-
 Class Affine {PROP : bi} (Q : PROP) := affine : Q âŠ¢ emp.
 Arguments Affine {_} _%I : simpl never.
 Arguments affine {_} _%I {_}.
@@ -72,9 +69,22 @@ Notation "'<affine>?' p P" := (bi_affinely_if p P)
   (at level 20, p at level 9, P at level 20,
    right associativity, format "'<affine>?' p  P") : bi_scope.
 
-Notation "â–¡? p P" := (<affine>?p <pers>?p P)%I
+Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
+  (<affine> <pers> P)%I.
+Arguments bi_intuitionistically {_} _%I : simpl never.
+Instance: Params (@bi_intuitionistically) 1.
+Typeclasses Opaque bi_intuitionistically.
+Notation "â–¡ P" := (bi_intuitionistically P)%I
+  (at level 20, right associativity) : bi_scope.
+
+Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then â–¡ P else P)%I.
+Arguments bi_intuitionistically_if {_} !_ _%I /.
+Instance: Params (@bi_intuitionistically_if) 2.
+Typeclasses Opaque bi_intuitionistically_if.
+Notation "'â–¡?' p P" := (bi_intuitionistically_if p P)
   (at level 20, p at level 9, P at level 20,
-   right associativity, format "â–¡? p  P") : bi_scope.
+   right associativity, format "'â–¡?' p  P") : bi_scope.
 
 Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP â†’ PROP :=
   match As return himpl As PROP â†’ PROP with
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index a00d21347..f4802b066 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -879,7 +879,7 @@ Qed.
 Lemma impl_wand_persistently_2 P Q : (<pers> P -âˆ— Q) âŠ¢ (<pers> P â†’ Q).
 Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
 
-Section persistently_affinely_bi.
+Section persistently_affine_bi.
   Context `{BiAffine PROP}.
 
   Lemma persistently_emp : <pers> emp âŠ£âŠ¢ emp.
@@ -926,72 +926,114 @@ Section persistently_affinely_bi.
     - apply exist_elim=> R. apply impl_intro_l.
       by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r.
   Qed.
-End persistently_affinely_bi.
+End persistently_affine_bi.
 
-(* The combined affinely persistently modality *)
-Lemma affinely_persistently_elim P : â–¡ P âŠ¢ P.
+(* The intuitionistic modality *)
+Global Instance intuitionistically_ne : NonExpansive (@bi_intuitionistically PROP).
+Proof. solve_proper. Qed.
+Global Instance intuitionistically_proper : Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@bi_intuitionistically PROP).
+Proof. solve_proper. Qed.
+Global Instance intuitionistically_mono' : Proper ((âŠ¢) ==> (âŠ¢)) (@bi_intuitionistically PROP).
+Proof. solve_proper. Qed.
+Global Instance intuitionistically_flip_mono' :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@bi_intuitionistically PROP).
+Proof. solve_proper. Qed.
+
+Lemma intuitionistically_elim P : â–¡ P âŠ¢ P.
 Proof. apply persistently_and_emp_elim. Qed.
-Lemma affinely_persistently_intro' P Q : (â–¡ P âŠ¢ Q) â†’ â–¡ P âŠ¢ â–¡ Q.
-Proof. intros <-. by rewrite persistently_affinely persistently_idemp. Qed.
+Lemma intuitionistically_elim_emp P : â–¡ P âŠ¢ emp.
+Proof. rewrite /bi_intuitionistically affinely_elim_emp //. Qed.
+Lemma intuitionistically_intro' P Q : (â–¡ P âŠ¢ Q) â†’ â–¡ P âŠ¢ â–¡ Q.
+Proof.
+  intros <-.
+  by rewrite /bi_intuitionistically persistently_affinely persistently_idemp.
+Qed.
 
-Lemma affinely_persistently_emp : â–¡ emp âŠ£âŠ¢ emp.
+Lemma intuitionistically_emp : â–¡ emp âŠ£âŠ¢ emp.
+Proof.
+  by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
+             affinely_True_emp affinely_emp.
+Qed.
+Lemma intuitionistically_True_emp : â–¡ True âŠ£âŠ¢ emp.
 Proof.
-  by rewrite -persistently_True_emp persistently_pure affinely_True_emp
-             affinely_emp.
+  rewrite -intuitionistically_emp /bi_intuitionistically
+    persistently_True_emp //.
 Qed.
-Lemma affinely_persistently_and P Q : â–¡ (P âˆ§ Q) âŠ£âŠ¢ â–¡ P âˆ§ â–¡ Q.
-Proof. by rewrite persistently_and affinely_and. Qed.
-Lemma affinely_persistently_or P Q : â–¡ (P âˆ¨ Q) âŠ£âŠ¢ â–¡ P âˆ¨ â–¡ Q.
-Proof. by rewrite persistently_or affinely_or. Qed.
-Lemma affinely_persistently_exist {A} (Î¦ : A â†’ PROP) : â–¡ (âˆƒ x, Î¦ x) âŠ£âŠ¢ âˆƒ x, â–¡ Î¦ x.
-Proof. by rewrite persistently_exist affinely_exist. Qed.
-Lemma affinely_persistently_sep_2 P Q : â–¡ P âˆ— â–¡ Q âŠ¢ â–¡ (P âˆ— Q).
-Proof. by rewrite affinely_sep_2 persistently_sep_2. Qed.
-Lemma affinely_persistently_sep `{BiPositive PROP} P Q : â–¡ (P âˆ— Q) âŠ£âŠ¢ â–¡ P âˆ— â–¡ Q.
-Proof. by rewrite -affinely_sep -persistently_sep. Qed.
+Lemma intuitionistically_and P Q : â–¡ (P âˆ§ Q) âŠ£âŠ¢ â–¡ P âˆ§ â–¡ Q.
+Proof. by rewrite /bi_intuitionistically persistently_and affinely_and. Qed.
+Lemma intuitionistically_or P Q : â–¡ (P âˆ¨ Q) âŠ£âŠ¢ â–¡ P âˆ¨ â–¡ Q.
+Proof. by rewrite /bi_intuitionistically persistently_or affinely_or. Qed.
+Lemma intuitionistically_exist {A} (Î¦ : A â†’ PROP) : â–¡ (âˆƒ x, Î¦ x) âŠ£âŠ¢ âˆƒ x, â–¡ Î¦ x.
+Proof. by rewrite /bi_intuitionistically persistently_exist affinely_exist. Qed.
+Lemma intuitionistically_sep_2 P Q : â–¡ P âˆ— â–¡ Q âŠ¢ â–¡ (P âˆ— Q).
+Proof. by rewrite /bi_intuitionistically affinely_sep_2 persistently_sep_2. Qed.
+Lemma intuitionistically_sep `{BiPositive PROP} P Q : â–¡ (P âˆ— Q) âŠ£âŠ¢ â–¡ P âˆ— â–¡ Q.
+Proof. by rewrite /bi_intuitionistically -affinely_sep -persistently_sep. Qed.
 
-Lemma affinely_persistently_idemp P : â–¡ â–¡ P âŠ£âŠ¢ â–¡ P.
-Proof. by rewrite persistently_affinely persistently_idemp. Qed.
+Lemma intuitionistically_idemp P : â–¡ â–¡ P âŠ£âŠ¢ â–¡ P.
+Proof. by rewrite /bi_intuitionistically persistently_affinely persistently_idemp. Qed.
 
-Lemma persistently_and_affinely_sep_l P Q : <pers> P âˆ§ Q âŠ£âŠ¢ â–¡ P âˆ— Q.
+Lemma intuitionistically_persistently_1 P : â–¡ P âŠ¢ <pers> P.
+Proof. rewrite /bi_intuitionistically affinely_elim //. Qed.
+Lemma intuitionistically_persistently_persistently P : â–¡ <pers> P âŠ£âŠ¢ â–¡ P.
+Proof. rewrite /bi_intuitionistically persistently_idemp //. Qed.
+
+Lemma intuitionistically_affinely P : â–¡ P âŠ¢ <affine> P.
 Proof.
-  apply (anti_symm _).
+  rewrite /bi_intuitionistically /bi_affinely. apply and_intro.
+  - rewrite and_elim_l //.
+  - apply persistently_and_emp_elim.
+Qed.
+Lemma intuitionistically_affinely_affinely P : â–¡ <affine> P âŠ£âŠ¢ â–¡ P.
+Proof. rewrite /bi_intuitionistically persistently_affinely //. Qed.
+
+Lemma persistently_and_intuitionistically_sep_l P Q : <pers> P âˆ§ Q âŠ£âŠ¢ â–¡ P âˆ— Q.
+Proof.
+  rewrite /bi_intuitionistically. apply (anti_symm _).
   - by rewrite /bi_affinely -(comm bi_and (<pers> P)%I)
       -persistently_and_sep_assoc left_id.
   - apply and_intro.
     + by rewrite affinely_elim persistently_absorbing.
     + by rewrite affinely_elim_emp left_id.
 Qed.
-Lemma persistently_and_affinely_sep_r P Q : P âˆ§ <pers> Q âŠ£âŠ¢ P âˆ— â–¡ Q.
-Proof. by rewrite !(comm _ P) persistently_and_affinely_sep_l. Qed.
-Lemma and_sep_affinely_persistently P Q : â–¡ P âˆ§ â–¡ Q âŠ£âŠ¢ â–¡ P âˆ— â–¡ Q.
+Lemma persistently_and_intuitionistically_sep_r P Q : P âˆ§ <pers> Q âŠ£âŠ¢ P âˆ— â–¡ Q.
+Proof. by rewrite !(comm _ P) persistently_and_intuitionistically_sep_l. Qed.
+Lemma and_sep_intuitionistically P Q : â–¡ P âˆ§ â–¡ Q âŠ£âŠ¢ â–¡ P âˆ— â–¡ Q.
 Proof.
-  by rewrite -persistently_and_affinely_sep_l -affinely_and affinely_and_r.
+  by rewrite -persistently_and_intuitionistically_sep_l -affinely_and affinely_and_r.
 Qed.
 
-Lemma affinely_persistently_sep_dup P : â–¡ P âŠ£âŠ¢ â–¡ P âˆ— â–¡ P.
+Lemma intuitionistically_sep_dup P : â–¡ P âŠ£âŠ¢ â–¡ P âˆ— â–¡ P.
 Proof.
-  by rewrite -persistently_and_affinely_sep_l affinely_and_r idemp.
+  by rewrite -persistently_and_intuitionistically_sep_l affinely_and_r idemp.
 Qed.
 
-Lemma impl_wand_affinely_persistently P Q : (<pers> P â†’ Q) âŠ£âŠ¢ (â–¡ P -âˆ— Q).
+Lemma impl_wand_intuitionistically P Q : (<pers> P â†’ Q) âŠ£âŠ¢ (â–¡ P -âˆ— Q).
 Proof.
   apply (anti_symm (âŠ¢)).
-  - apply wand_intro_l. by rewrite -persistently_and_affinely_sep_l impl_elim_r.
-  - apply impl_intro_l. by rewrite persistently_and_affinely_sep_l wand_elim_r.
+  - apply wand_intro_l. by rewrite -persistently_and_intuitionistically_sep_l impl_elim_r.
+  - apply impl_intro_l. by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
 Qed.
 
-Lemma affinely_persistently_alt_fixpoint P :
+Lemma intuitionistically_alt_fixpoint P :
   â–¡ P âŠ£âŠ¢ emp âˆ§ (P âˆ— â–¡ P).
 Proof.
   apply (anti_symm (âŠ¢)).
   - apply and_intro; first exact: affinely_elim_emp.
-    rewrite {1}affinely_persistently_sep_dup. apply sep_mono; last done.
-    apply affinely_persistently_elim.
-  - apply and_mono; first done. rewrite {2}persistently_alt_fixpoint.
+    rewrite {1}intuitionistically_sep_dup. apply sep_mono; last done.
+    apply intuitionistically_elim.
+  - apply and_mono; first done. rewrite /bi_intuitionistically {2}persistently_alt_fixpoint.
     apply sep_mono; first done. apply and_elim_r.
 Qed.
 
+
+Section bi_affine_intuitionistically.
+  Context `{BiAffine PROP}.
+
+  Lemma intuitionistically_persistently P : â–¡ P âŠ£âŠ¢ <pers> P.
+  Proof. rewrite /bi_intuitionistically affine_affinely //. Qed.
+End bi_affine_intuitionistically.
+
 (* Conditional affinely modality *)
 Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
@@ -1067,37 +1109,49 @@ Proof. destruct p; simpl; auto using persistently_sep. Qed.
 Lemma persistently_if_idemp p P : <pers>?p <pers>?p P âŠ£âŠ¢ <pers>?p P.
 Proof. destruct p; simpl; auto using persistently_idemp. Qed.
 
-(* Conditional affinely persistently *)
-Lemma affinely_persistently_if_mono p P Q : (P âŠ¢ Q) â†’ â–¡?p P âŠ¢ â–¡?p Q.
+(* Conditional intuitionistically *)
+Global Instance intuitionistically_if_ne p : NonExpansive (@bi_intuitionistically_if PROP p).
+Proof. solve_proper. Qed.
+Global Instance intuitionistically_if_proper p :
+  Proper ((âŠ£âŠ¢) ==> (âŠ£âŠ¢)) (@bi_intuitionistically_if PROP p).
+Proof. solve_proper. Qed.
+Global Instance intuitionistically_if_mono' p :
+  Proper ((âŠ¢) ==> (âŠ¢)) (@bi_intuitionistically_if PROP p).
+Proof. solve_proper. Qed.
+Global Instance intuitionistically_if_flip_mono' p :
+  Proper (flip (âŠ¢) ==> flip (âŠ¢)) (@bi_intuitionistically_if PROP p).
+Proof. solve_proper. Qed.
+
+Lemma intuitionistically_if_mono p P Q : (P âŠ¢ Q) â†’ â–¡?p P âŠ¢ â–¡?p Q.
 Proof. by intros ->. Qed.
-Lemma affinely_persistently_if_flag_mono (p q : bool) P :
+Lemma intuitionistically_if_flag_mono (p q : bool) P :
   (q â†’ p) â†’ â–¡?p P âŠ¢ â–¡?q P.
-Proof. destruct p, q; naive_solver auto using affinely_persistently_elim. Qed.
-
-Lemma affinely_persistently_if_elim p P : â–¡?p P âŠ¢ P.
-Proof. destruct p; simpl; auto using affinely_persistently_elim. Qed.
-Lemma affinely_persistently_affinely_persistently_if p P : â–¡ P âŠ¢ â–¡?p P.
-Proof. destruct p; simpl; auto using affinely_persistently_elim. Qed.
-Lemma affinely_persistently_if_intro' p P Q : (â–¡?p P âŠ¢ Q) â†’ â–¡?p P âŠ¢ â–¡?p Q.
-Proof. destruct p; simpl; auto using affinely_persistently_intro'. Qed.
-
-Lemma affinely_persistently_if_emp p : â–¡?p emp âŠ£âŠ¢ emp.
-Proof. destruct p; simpl; auto using affinely_persistently_emp. Qed.
-Lemma affinely_persistently_if_and p P Q : â–¡?p (P âˆ§ Q) âŠ£âŠ¢ â–¡?p P âˆ§ â–¡?p Q.
-Proof. destruct p; simpl; auto using affinely_persistently_and. Qed.
-Lemma affinely_persistently_if_or p P Q : â–¡?p (P âˆ¨ Q) âŠ£âŠ¢ â–¡?p P âˆ¨ â–¡?p Q.
-Proof. destruct p; simpl; auto using affinely_persistently_or. Qed.
-Lemma affinely_persistently_if_exist {A} p (Î¨ : A â†’ PROP) :
+Proof. destruct p, q; naive_solver auto using intuitionistically_elim. Qed.
+
+Lemma intuitionistically_if_elim p P : â–¡?p P âŠ¢ P.
+Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.
+Lemma intuitionistically_intuitionistically_if p P : â–¡ P âŠ¢ â–¡?p P.
+Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.
+Lemma intuitionistically_if_intro' p P Q : (â–¡?p P âŠ¢ Q) â†’ â–¡?p P âŠ¢ â–¡?p Q.
+Proof. destruct p; simpl; auto using intuitionistically_intro'. Qed.
+
+Lemma intuitionistically_if_emp p : â–¡?p emp âŠ£âŠ¢ emp.
+Proof. destruct p; simpl; auto using intuitionistically_emp. Qed.
+Lemma intuitionistically_if_and p P Q : â–¡?p (P âˆ§ Q) âŠ£âŠ¢ â–¡?p P âˆ§ â–¡?p Q.
+Proof. destruct p; simpl; auto using intuitionistically_and. Qed.
+Lemma intuitionistically_if_or p P Q : â–¡?p (P âˆ¨ Q) âŠ£âŠ¢ â–¡?p P âˆ¨ â–¡?p Q.
+Proof. destruct p; simpl; auto using intuitionistically_or. Qed.
+Lemma intuitionistically_if_exist {A} p (Î¨ : A â†’ PROP) :
   (â–¡?p âˆƒ a, Î¨ a) âŠ£âŠ¢ âˆƒ a, â–¡?p Î¨ a.
-Proof. destruct p; simpl; auto using affinely_persistently_exist. Qed.
-Lemma affinely_persistently_if_sep_2 p P Q : â–¡?p P âˆ— â–¡?p Q âŠ¢ â–¡?p (P âˆ— Q).
-Proof. destruct p; simpl; auto using affinely_persistently_sep_2. Qed.
-Lemma affinely_persistently_if_sep `{BiPositive PROP} p P Q :
+Proof. destruct p; simpl; auto using intuitionistically_exist. Qed.
+Lemma intuitionistically_if_sep_2 p P Q : â–¡?p P âˆ— â–¡?p Q âŠ¢ â–¡?p (P âˆ— Q).
+Proof. destruct p; simpl; auto using intuitionistically_sep_2. Qed.
+Lemma intuitionistically_if_sep `{BiPositive PROP} p P Q :
   â–¡?p (P âˆ— Q) âŠ£âŠ¢ â–¡?p P âˆ— â–¡?p Q.
-Proof. destruct p; simpl; auto using affinely_persistently_sep. Qed.
+Proof. destruct p; simpl; auto using intuitionistically_sep. Qed.
 
-Lemma affinely_persistently_if_idemp p P : â–¡?p â–¡?p P âŠ£âŠ¢ â–¡?p P.
-Proof. destruct p; simpl; auto using affinely_persistently_idemp. Qed.
+Lemma intuitionistically_if_idemp p P : â–¡?p â–¡?p P âŠ£âŠ¢ â–¡?p P.
+Proof. destruct p; simpl; auto using intuitionistically_idemp. Qed.
 
 (* Properties of persistent propositions *)
 Global Instance Persistent_proper : Proper ((â‰¡) ==> iff) (@Persistent PROP).
@@ -1114,18 +1168,18 @@ Lemma persistently_intro P Q `{!Persistent P} : (P âŠ¢ Q) â†’ P âŠ¢ <pers> Q.
 Proof. intros HP. by rewrite (persistent P) HP. Qed.
 Lemma persistent_and_affinely_sep_l_1 P Q `{!Persistent P} : P âˆ§ Q âŠ¢ <affine> P âˆ— Q.
 Proof.
-  rewrite {1}(persistent_persistently_2 P) persistently_and_affinely_sep_l.
-  by rewrite -affinely_idemp affinely_persistently_elim.
+  rewrite {1}(persistent_persistently_2 P) persistently_and_intuitionistically_sep_l.
+  rewrite intuitionistically_affinely //.
 Qed.
 Lemma persistent_and_affinely_sep_r_1 P Q `{!Persistent Q} : P âˆ§ Q âŠ¢ P âˆ— <affine> Q.
 Proof. by rewrite !(comm _ P) persistent_and_affinely_sep_l_1. Qed.
 
 Lemma persistent_and_affinely_sep_l P Q `{!Persistent P, !Absorbing P} :
   P âˆ§ Q âŠ£âŠ¢ <affine> P âˆ— Q.
-Proof. by rewrite -(persistent_persistently P) persistently_and_affinely_sep_l. Qed.
+Proof. by rewrite -(persistent_persistently P) persistently_and_intuitionistically_sep_l. Qed.
 Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
   P âˆ§ Q âŠ£âŠ¢ P âˆ— <affine> Q.
-Proof. by rewrite -(persistent_persistently Q) persistently_and_affinely_sep_r. Qed.
+Proof. by rewrite -(persistent_persistently Q) persistently_and_intuitionistically_sep_r. Qed.
 
 Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
   P âˆ§ Q âŠ¢ P âˆ— Q.
@@ -1143,24 +1197,24 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 Lemma persistent_entails_r P Q `{!Persistent Q} : (P âŠ¢ Q) â†’ P âŠ¢ P âˆ— Q.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 
-Lemma absorbingly_affinely_persistently P : <absorb> â–¡ P âŠ£âŠ¢ <pers> P.
+Lemma absorbingly_intuitionistically P : <absorb> â–¡ P âŠ£âŠ¢ <pers> P.
 Proof.
   apply (anti_symm _).
-  - by rewrite affinely_elim absorbingly_persistently.
-  - rewrite -{1}(idemp bi_and (<pers> _)%I) persistently_and_affinely_sep_r.
+  - by rewrite intuitionistically_persistently_1 absorbingly_persistently.
+  - rewrite -{1}(idemp bi_and (<pers> _)%I) persistently_and_intuitionistically_sep_r.
     by rewrite {1} (True_intro (<pers> _)%I).
 Qed.
 
 Lemma persistent_absorbingly_affinely_2 P `{!Persistent P} :
   P âŠ¢ <absorb> <affine> P.
 Proof.
-  rewrite {1}(persistent P) -absorbingly_affinely_persistently.
-  by rewrite -{1}affinely_idemp affinely_persistently_elim.
+  rewrite {1}(persistent P) -absorbingly_intuitionistically.
+  by rewrite intuitionistically_affinely.
 Qed.
 Lemma persistent_absorbingly_affinely P `{!Persistent P, !Absorbing P} :
   <absorb> <affine> P âŠ£âŠ¢ P.
 Proof.
-  by rewrite -(persistent_persistently P) absorbingly_affinely_persistently.
+  by rewrite -(persistent_persistently P) absorbingly_intuitionistically.
 Qed.
 
 Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
@@ -1205,6 +1259,8 @@ Global Instance sep_affine P Q : Affine P â†’ Affine Q â†’ Affine (P âˆ— Q).
 Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
 Global Instance affinely_affine P : Affine (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance intuitionistically_affine P : Affine (â–¡ P).
+Proof. rewrite /bi_intuitionistically. apply _. Qed.
 
 (* Absorbing instances *)
 Global Instance pure_absorbing Ï† : Absorbing (âŒœÏ†âŒ%I : PROP).
@@ -1282,6 +1338,8 @@ Global Instance persistently_persistent P : Persistent (<pers> P).
 Proof. by rewrite /Persistent persistently_idemp. Qed.
 Global Instance affinely_persistent P : Persistent P â†’ Persistent (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance intuitionistically_persistent P : Persistent (â–¡ P).
+Proof. rewrite /bi_intuitionistically. apply _. Qed.
 Global Instance absorbingly_persistent P : Persistent P â†’ Persistent (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance from_option_persistent {A} P (Î¨ : A â†’ PROP) (mx : option A) :
@@ -1565,10 +1623,10 @@ Lemma later_persistently P : â–· <pers> P âŠ£âŠ¢ <pers> â–· P.
 Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
 Lemma later_affinely_2 P : <affine> â–· P âŠ¢ â–· <affine> P.
 Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
-Lemma later_affinely_persistently_2 P : â–¡ â–· P âŠ¢ â–· â–¡ P.
-Proof. by rewrite -later_persistently later_affinely_2. Qed.
-Lemma later_affinely_persistently_if_2 p P : â–¡?p â–· P âŠ¢ â–· â–¡?p P.
-Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed.
+Lemma later_intuitionistically_2 P : â–¡ â–· P âŠ¢ â–· â–¡ P.
+Proof. by rewrite /bi_intuitionistically -later_persistently later_affinely_2. Qed.
+Lemma later_intuitionistically_if_2 p P : â–¡?p â–· P âŠ¢ â–· â–¡?p P.
+Proof. destruct p; simpl; auto using later_intuitionistically_2. Qed.
 Lemma later_absorbingly P : â–· <absorb> P âŠ£âŠ¢ <absorb> â–· P.
 Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
 
@@ -1632,10 +1690,10 @@ Lemma laterN_persistently n P : â–·^n <pers> P âŠ£âŠ¢ <pers> â–·^n P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
 Lemma laterN_affinely_2 n P : <affine> â–·^n P âŠ¢ â–·^n <affine> P.
 Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
-Lemma laterN_affinely_persistently_2 n P : â–¡ â–·^n P âŠ¢ â–·^n â–¡ P.
-Proof. by rewrite -laterN_persistently laterN_affinely_2. Qed.
-Lemma laterN_affinely_persistently_if_2 n p P : â–¡?p â–·^n P âŠ¢ â–·^n â–¡?p P.
-Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed.
+Lemma laterN_intuitionistically_2 n P : â–¡ â–·^n P âŠ¢ â–·^n â–¡ P.
+Proof. by rewrite /bi_intuitionistically -laterN_persistently laterN_affinely_2. Qed.
+Lemma laterN_intuitionistically_if_2 n p P : â–¡?p â–·^n P âŠ¢ â–·^n â–¡?p P.
+Proof. destruct p; simpl; auto using laterN_intuitionistically_2. Qed.
 Lemma laterN_absorbingly n P : â–·^n <absorb> P âŠ£âŠ¢ <absorb> â–·^n P.
 Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
 
@@ -1707,10 +1765,10 @@ Proof.
 Qed.
 Lemma except_0_affinely_2 P : <affine> â—‡ P âŠ¢ â—‡ <affine> P.
 Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
-Lemma except_0_affinely_persistently_2 P : â–¡ â—‡ P âŠ¢ â—‡ â–¡ P.
-Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed.
-Lemma except_0_affinely_persistently_if_2 p P : â–¡?p â—‡ P âŠ¢ â—‡ â–¡?p P.
-Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed.
+Lemma except_0_intuitionistically_2 P : â–¡ â—‡ P âŠ¢ â—‡ â–¡ P.
+Proof. by rewrite /bi_intuitionistically -except_0_persistently except_0_affinely_2. Qed.
+Lemma except_0_intuitionistically_if_2 p P : â–¡?p â—‡ P âŠ¢ â—‡ â–¡?p P.
+Proof. destruct p; simpl; auto using except_0_intuitionistically_2. Qed.
 Lemma except_0_absorbingly P : â—‡ <absorb> P âŠ£âŠ¢ <absorb> â—‡ P.
 Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
 
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 247c09ff7..d7ea67739 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -145,10 +145,14 @@ Section embed.
   Proof. by rewrite embed_and embed_emp. Qed.
   Lemma embed_absorbingly P : âŽ¡<absorb> PâŽ¤ âŠ£âŠ¢ <absorb> âŽ¡PâŽ¤.
   Proof. by rewrite embed_sep embed_pure. Qed.
+  Lemma embed_intuitionistically P : âŽ¡â–¡ PâŽ¤ âŠ£âŠ¢ â–¡ âŽ¡PâŽ¤.
+  Proof. rewrite embed_and embed_emp embed_persistently //. Qed.
   Lemma embed_persistently_if P b : âŽ¡<pers>?b PâŽ¤ âŠ£âŠ¢ <pers>?b âŽ¡PâŽ¤.
   Proof. destruct b; simpl; auto using embed_persistently. Qed.
   Lemma embed_affinely_if P b : âŽ¡<affine>?b PâŽ¤ âŠ£âŠ¢ <affine>?b âŽ¡PâŽ¤.
   Proof. destruct b; simpl; auto using embed_affinely. Qed.
+  Lemma embed_intuitionistically_if P b : âŽ¡â–¡?b PâŽ¤ âŠ£âŠ¢ â–¡?b âŽ¡PâŽ¤.
+  Proof. destruct b; simpl; auto using embed_intuitionistically. Qed.
   Lemma embed_hforall {As} (Î¦ : himpl As PROP1):
     âŽ¡bi_hforall Î¦âŽ¤ âŠ£âŠ¢ bi_hforall (hcompose embed Î¦).
   Proof. induction As=>//. rewrite /= embed_forall. by do 2 f_equiv. Qed.
diff --git a/theories/bi/fixpoint.v b/theories/bi/fixpoint.v
index 43f506b7b..fff0a31fc 100644
--- a/theories/bi/fixpoint.v
+++ b/theories/bi/fixpoint.v
@@ -85,7 +85,8 @@ Section greatest.
     F (bi_greatest_fixpoint F) x âŠ¢ bi_greatest_fixpoint F x.
   Proof.
     iIntros "HF". iExists (CofeMor (F (bi_greatest_fixpoint F))).
-    iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
+    (* FIXME: The framing here adds an <affine> modality that we have to introduce. *)
+    iIntros "{$HF} !# !#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
     iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
   Qed.
 
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 7d1074804..192db2027 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -173,6 +173,6 @@ Section fractional.
     - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
     - rewrite fractional /Frame /MakeSep=><-<-=>_.
       by rewrite (comm _ Q (Î¦ q0)) !assoc (comm _ (Î¦ _)).
-    - move=>-[-> _]->. by rewrite bi.affinely_persistently_if_elim -fractional Qp_div_2.
+    - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp_div_2.
   Qed.
 End fractional.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index d6ea57fc1..194cfe311 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -637,12 +637,16 @@ Proof. intros i j. unseal. by rewrite objective_at. Qed.
 
 Global Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance intuitionistically_objective P `{!Objective P} : Objective (â–¡ P).
+Proof. rewrite /bi_intuitionistically. apply _. Qed.
 Global Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance persistently_if_objective P p `{!Objective P} : Objective (<pers>?p P).
 Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
 Global Instance affinely_if_objective P p `{!Objective P} : Objective (<affine>?p P).
 Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
+Global Instance intuitionistically_if_objective P p `{!Objective P} : Objective (<affine>?p P).
+Proof. rewrite /bi_intuitionistically_if. destruct p; apply _. Qed.
 
 (** monPred_in *)
 Lemma monPred_in_intro P : P âŠ¢ âˆƒ i, monPred_in i âˆ§ âŽ¡P iâŽ¤.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 0011b8270..13198641e 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -119,7 +119,7 @@ Global Instance plainly_flip_mono' :
 Proof. intros P Q; apply plainly_mono. Qed.
 
 Lemma affinely_plainly_elim P : <affine> â–  P âŠ¢ P.
-Proof. by rewrite plainly_elim_persistently affinely_persistently_elim. Qed.
+Proof. by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim. Qed.
 
 Lemma persistently_plainly P : <pers> â–  P âŠ£âŠ¢ â–  P.
 Proof.
@@ -216,6 +216,14 @@ Qed.
 Lemma plainly_affinely P : â–  <affine> P âŠ£âŠ¢ â–  P.
 Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
 
+Lemma intuitionistically_plainly_elim P : â–¡ â–  P -âˆ— â–¡ P.
+Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
+Lemma intuitionistically_plainly P : â–¡ â–  P -âˆ— â–  â–¡ P.
+Proof.
+  rewrite /bi_intuitionistically plainly_affinely affinely_elim.
+  rewrite persistently_plainly plainly_persistently. done.
+Qed.
+
 Lemma and_sep_plainly P Q : â–  P âˆ§ â–  Q âŠ£âŠ¢ â–  P âˆ— â–  Q.
 Proof.
   apply (anti_symm _); auto using plainly_and_sep_l_1.
@@ -252,7 +260,7 @@ Lemma impl_wand_plainly_2 P Q : (â–  P -âˆ— Q) âŠ¢ (â–  P â†’ Q).
 Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
 
 Lemma impl_wand_affinely_plainly P Q : (â–  P â†’ Q) âŠ£âŠ¢ (<affine> â–  P -âˆ— Q).
-Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed.
+Proof. by rewrite -(persistently_plainly P) impl_wand_intuitionistically. Qed.
 
 Lemma persistently_wand_affinely_plainly P Q :
   (<affine> â–  P -âˆ— <pers> Q) âŠ¢ <pers> (<affine> â–  P -âˆ— Q).
@@ -441,6 +449,8 @@ Proof.
 Qed.
 Global Instance affinely_plain P : Plain P â†’ Plain (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance intuitionistically_plain P : Plain P â†’ Plain (â–¡ P).
+Proof. rewrite /bi_intuitionistically. apply _. Qed.
 Global Instance absorbingly_plain P : Plain P â†’ Plain (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance from_option_plain {A} P (Î¨ : A â†’ PROP) (mx : option A) :
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 7471c3794..331ba1db0 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -76,7 +76,7 @@ Section increment_client.
                            âŠ¤ âŠ¤
                            (Î» _ _, True))%I as "#Aupd".
     { iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
-      iIntros (E) "!# % _".
+      iIntros "!#" (E) "% _".
       assert (E = âŠ¤) as -> by set_solver.
       iInv nroot as (x) ">Hâ†¦" "Hclose".
       iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f24e279eb..a271c1fcf 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -24,13 +24,13 @@ Proof. by rewrite /IntoAbsorbingly. Qed.
 
 (* FromAssumption *)
 Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
-Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
+Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
 
 Global Instance from_assumption_persistently_r P Q :
   FromAssumption true P Q â†’ KnownRFromAssumption true P (<pers> Q).
 Proof.
   rewrite /KnownRFromAssumption /FromAssumption /= =><-.
-  by rewrite -{1}affinely_persistently_idemp affinely_elim.
+  apply intuitionistically_persistent.
 Qed.
 Global Instance from_assumption_affinely_r P Q :
   FromAssumption true P Q â†’ KnownRFromAssumption true P (<affine> Q).
@@ -38,6 +38,12 @@ Proof.
   rewrite /KnownRFromAssumption /FromAssumption /= =><-.
   by rewrite affinely_idemp.
 Qed.
+Global Instance from_assumption_intuitionistically_r P Q :
+  FromAssumption true P Q â†’ KnownRFromAssumption true P (â–¡ Q).
+Proof.
+  rewrite /KnownRFromAssumption /FromAssumption /= =><-.
+  by rewrite intuitionistically_idemp.
+Qed.
 Global Instance from_assumption_absorbingly_r p P Q :
   FromAssumption p P Q â†’ KnownRFromAssumption p P (<absorb> Q).
 Proof.
@@ -45,23 +51,23 @@ Proof.
   apply absorbingly_intro.
 Qed.
 
-Global Instance from_assumption_affinely_persistently_l p P Q :
+Global Instance from_assumption_intuitionistically_l p P Q :
   FromAssumption true P Q â†’ KnownLFromAssumption p (â–¡ P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
-  by rewrite affinely_persistently_if_elim.
+  by rewrite intuitionistically_if_elim.
 Qed.
 Global Instance from_assumption_persistently_l_true P Q :
   FromAssumption true P Q â†’ KnownLFromAssumption true (<pers> P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
-  by rewrite persistently_idemp.
+  rewrite intuitionistically_persistently_persistently //.
 Qed.
 Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
   FromAssumption true P Q â†’ KnownLFromAssumption false (<pers> P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
-  by rewrite affine_affinely.
+  by rewrite intuitionistically_persistently.
 Qed.
 Global Instance from_assumption_affinely_l_true p P Q :
   FromAssumption p P Q â†’ KnownLFromAssumption p (<affine> P) Q.
@@ -203,6 +209,12 @@ Qed.
 Global Instance into_persistent_affinely p P Q :
   IntoPersistent p P Q â†’ IntoPersistent p (<affine> P) Q | 0.
 Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
+Global Instance into_persistent_intuitionistically p P Q :
+  IntoPersistent p P Q â†’ IntoPersistent p (â–¡ P) Q | 0.
+Proof. rewrite /IntoPersistent /= =><-. by rewrite intuitionistically_elim. Qed.
+Global Instance into_persistent_intuitionistically2 P Q :
+  IntoPersistent true P Q â†’ IntoPersistent false (â–¡ P) Q | 0.
+Proof. rewrite /IntoPersistent /= =><-. by rewrite intuitionistically_persistently_1. Qed.
 Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
   IntoPersistent p P Q â†’ IntoPersistent p âŽ¡PâŽ¤ âŽ¡QâŽ¤ | 0.
 Proof.
@@ -222,12 +234,12 @@ Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_persistently P :
   FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
 Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_affinely_persistently P :
-  FromModal modality_affinely_persistently (â–¡ P) (â–¡ P) P | 1.
+Global Instance from_modal_intuitionistically P :
+  FromModal modality_intuitionistically (â–¡ P) (â–¡ P) P | 1.
 Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_affinely_persistently_affine_bi P :
+Global Instance from_modal_intuitionistically_affine_bi P :
   BiAffine PROP â†’ FromModal modality_persistently (â–¡ P) (â–¡ P) P | 0.
-Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
+Proof. intros. by rewrite /FromModal /= intuitionistically_persistently. Qed.
 
 Global Instance from_modal_absorbingly P :
   FromModal modality_id (<absorb> P) (<absorb> P) P.
@@ -252,9 +264,9 @@ Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P
   FromModal modality_persistently sel P Q â†’
   FromModal modality_persistently sel âŽ¡PâŽ¤ âŽ¡QâŽ¤ | 100.
 Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
-Global Instance from_modal_affinely_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
-  FromModal modality_affinely_persistently sel P Q â†’
-  FromModal modality_affinely_persistently sel âŽ¡PâŽ¤ âŽ¡QâŽ¤ | 100.
+Global Instance from_modal_intuitionistically_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
+  FromModal modality_intuitionistically sel P Q â†’
+  FromModal modality_intuitionistically sel âŽ¡PâŽ¤ âŽ¡QâŽ¤ | 100.
 Proof.
   rewrite /FromModal /= =><-. by rewrite embed_affinely embed_persistently.
 Qed.
@@ -263,7 +275,7 @@ Qed.
 Global Instance into_wand_wand p q P Q P' :
   FromAssumption q P P' â†’ IntoWand p q (P' -âˆ— Q) P Q.
 Proof.
-  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
+  rewrite /FromAssumption /IntoWand=> HP. by rewrite HP intuitionistically_if_elim.
 Qed.
 Global Instance into_wand_impl_false_false P Q P' :
   Absorbing P' â†’ Absorbing (P' â†’ Q) â†’
@@ -277,23 +289,21 @@ Global Instance into_wand_impl_false_true P Q P' :
   IntoWand false true (P' â†’ Q) P Q.
 Proof.
   rewrite /IntoWand /FromAssumption /= => ? HP. apply wand_intro_l.
-  rewrite -(affinely_persistently_idemp P) HP.
-  by rewrite -persistently_and_affinely_sep_l persistently_elim impl_elim_r.
+  rewrite -(intuitionistically_idemp P) HP.
+  by rewrite -persistently_and_intuitionistically_sep_l persistently_elim impl_elim_r.
 Qed.
 Global Instance into_wand_impl_true_false P Q P' :
   Affine P' â†’ FromAssumption false P P' â†’
   IntoWand true false (P' â†’ Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
-  rewrite -persistently_and_affinely_sep_l HP -{2}(affine_affinely P') -affinely_and_lr.
-  by rewrite affinely_persistently_elim impl_elim_l.
+  rewrite HP sep_and intuitionistically_elim impl_elim_l //.
 Qed.
 Global Instance into_wand_impl_true_true P Q P' :
   FromAssumption true P P' â†’ IntoWand true true (P' â†’ Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => <-. apply wand_intro_l.
-  rewrite -{1}(affinely_persistently_idemp P) -and_sep_affinely_persistently.
-  by rewrite -affinely_persistently_and impl_elim_r affinely_persistently_elim.
+  rewrite sep_and [(â–¡ (_ â†’ _))%I]intuitionistically_elim impl_elim_r //.
 Qed.
 
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
@@ -306,35 +316,34 @@ Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_r. Qed.
 Global Instance into_wand_forall_prop_true p (Ï† : Prop) P :
   IntoWand p true (âˆ€ _ : Ï†, P) âŒœ Ï† âŒ P.
 Proof.
-  rewrite /IntoWand (affinely_persistently_if_elim p) /=
-          -impl_wand_affinely_persistently -pure_impl_forall
+  rewrite /IntoWand (intuitionistically_if_elim p) /=
+          -impl_wand_intuitionistically -pure_impl_forall
           bi.persistently_elim //.
 Qed.
 Global Instance into_wand_forall_prop_false p (Ï† : Prop) P :
   Absorbing P â†’ IntoWand p false (âˆ€ _ : Ï†, P) âŒœ Ï† âŒ P.
 Proof.
   intros ?.
-  rewrite /IntoWand (affinely_persistently_if_elim p) /= pure_wand_forall //.
+  rewrite /IntoWand (intuitionistically_if_elim p) /= pure_wand_forall //.
 Qed.
 
 Global Instance into_wand_forall {A} p q (Î¦ : A â†’ PROP) P Q x :
   IntoWand p q (Î¦ x) P Q â†’ IntoWand p q (âˆ€ x, Î¦ x) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
 
-Global Instance into_wand_affinely_persistently p q R P Q :
+Global Instance into_wand_intuitionistically p q R P Q :
   IntoWand p q R P Q â†’ IntoWand p q (â–¡ R) P Q.
-Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
+Proof. by rewrite /IntoWand intuitionistically_elim. Qed.
 Global Instance into_wand_persistently_true q R P Q :
   IntoWand true q R P Q â†’ IntoWand true q (<pers> R) P Q.
-Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
+Proof. by rewrite /IntoWand /= intuitionistically_persistently_persistently. Qed.
 Global Instance into_wand_persistently_false q R P Q :
   Absorbing R â†’ IntoWand false q R P Q â†’ IntoWand false q (<pers> R) P Q.
 Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
 Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
   IntoWand p q R P Q â†’ IntoWand p q âŽ¡RâŽ¤ âŽ¡PâŽ¤ âŽ¡QâŽ¤.
 Proof.
-  rewrite /IntoWand -!embed_persistently_if -!embed_affinely_if
-          -embed_wand => -> //.
+  rewrite /IntoWand -!embed_intuitionistically_if -embed_wand => -> //.
 Qed.
 
 (* FromWand *)
@@ -432,7 +441,7 @@ Proof. by rewrite /FromSep big_opL_app. Qed.
 
 (* IntoAnd *)
 Global Instance into_and_and p P Q : IntoAnd p (P âˆ§ Q) P Q | 10.
-Proof. by rewrite /IntoAnd affinely_persistently_if_and. Qed.
+Proof. by rewrite /IntoAnd intuitionistically_if_and. Qed.
 Global Instance into_and_and_affine_l P Q Q' :
   Affine P â†’ FromAffinely Q' Q â†’ IntoAnd false (P âˆ§ Q) P Q'.
 Proof.
@@ -448,7 +457,7 @@ Qed.
 
 Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P âˆ— Q) P Q.
 Proof.
-  by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
+  rewrite /IntoAnd /= intuitionistically_sep -and_sep_intuitionistically intuitionistically_and //.
 Qed.
 Global Instance into_and_sep_affine P Q :
   TCOr (Affine P) (Absorbing Q) â†’ TCOr (Absorbing P) (Affine Q) â†’
@@ -456,13 +465,13 @@ Global Instance into_and_sep_affine P Q :
 Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
 
 Global Instance into_and_pure p Ï† Ïˆ : @IntoAnd PROP p âŒœÏ† âˆ§ ÏˆâŒ âŒœÏ†âŒ âŒœÏˆâŒ.
-Proof. by rewrite /IntoAnd pure_and affinely_persistently_if_and. Qed.
+Proof. by rewrite /IntoAnd pure_and intuitionistically_if_and. Qed.
 
 Global Instance into_and_affinely p P Q1 Q2 :
   IntoAnd p P Q1 Q2 â†’ IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
 Proof.
   rewrite /IntoAnd. destruct p; simpl.
-  - by rewrite -affinely_and !persistently_affinely.
+  - rewrite -affinely_and !intuitionistically_affinely_affinely //.
   - intros ->. by rewrite affinely_and.
 Qed.
 Global Instance into_and_persistently p P Q1 Q2 :
@@ -470,14 +479,13 @@ Global Instance into_and_persistently p P Q1 Q2 :
   IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof.
   rewrite /IntoAnd /=. destruct p; simpl.
-  - by rewrite -persistently_and !persistently_idemp.
+  - rewrite -persistently_and !intuitionistically_persistently_persistently //.
   - intros ->. by rewrite persistently_and.
 Qed.
 Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
   IntoAnd p P Q1 Q2 â†’ IntoAnd p âŽ¡PâŽ¤ âŽ¡Q1âŽ¤ âŽ¡Q2âŽ¤.
 Proof.
-  rewrite /IntoAnd -embed_and -!embed_persistently_if
-          -!embed_affinely_if=> -> //.
+  rewrite /IntoAnd -embed_and -!embed_intuitionistically_if=> -> //.
 Qed.
 
 (* IntoSep *)
@@ -537,13 +545,13 @@ Proof.
   rewrite /IntoSep /= => -> ??.
   by rewrite sep_and persistently_and persistently_and_sep_l_1.
 Qed.
-Global Instance into_sep_affinely_persistently_affine P Q1 Q2 :
+Global Instance into_sep_intuitionistically_affine P Q1 Q2 :
   IntoSep P Q1 Q2 â†’
   TCOr (Affine Q1) (Absorbing Q2) â†’ TCOr (Absorbing Q1) (Affine Q2) â†’
   IntoSep (â–¡ P) (â–¡ Q1) (â–¡ Q2).
 Proof.
   rewrite /IntoSep /= => -> ??.
-  by rewrite sep_and affinely_persistently_and and_sep_affinely_persistently.
+  by rewrite sep_and intuitionistically_and and_sep_intuitionistically.
 Qed.
 
 (* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
@@ -756,25 +764,25 @@ Proof. by rewrite /AddModal !embed_bupd. Qed.
 
 (* Frame *)
 Global Instance frame_here_absorbing p R : Absorbing R â†’ Frame p R R True | 0.
-Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
+Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
 Global Instance frame_here p R : Frame p R R emp | 1.
-Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
+Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
 Global Instance frame_affinely_here_absorbing p R :
   Absorbing R â†’ Frame p (<affine> R) R True | 0.
 Proof.
-  intros. rewrite /Frame affinely_persistently_if_elim affinely_elim.
+  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
   apply sep_elim_l, _.
 Qed.
 Global Instance frame_affinely_here p R : Frame p (<affine> R) R emp | 1.
 Proof.
-  intros. rewrite /Frame affinely_persistently_if_elim affinely_elim.
+  intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
   apply sep_elim_l, _.
 Qed.
 
 Global Instance frame_here_pure p Ï† Q : FromPure false Q Ï† â†’ Frame p âŒœÏ†âŒ Q True.
 Proof.
   rewrite /FromPure /Frame=> <-.
-  by rewrite affinely_persistently_if_elim sep_elim_l.
+  by rewrite intuitionistically_if_elim sep_elim_l.
 Qed.
 
 Global Instance make_embed_pure `{BiEmbed PROP PROP'} Ï† :
@@ -791,7 +799,7 @@ Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
   Frame p R P Q â†’ MakeEmbed Q Q' â†’ Frame p âŽ¡RâŽ¤ âŽ¡PâŽ¤ Q'.
 Proof.
   rewrite /Frame /MakeEmbed => <- <-.
-  rewrite embed_sep embed_affinely_if embed_persistently_if => //.
+  rewrite embed_sep embed_intuitionistically_if => //.
 Qed.
 Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') Ï† :
   Frame p âŒœÏ†âŒ P Q â†’ MakeEmbed Q Q' â†’ Frame p âŒœÏ†âŒ âŽ¡PâŽ¤ Q'.
@@ -817,7 +825,7 @@ Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
   Frame true R (P1 âˆ— P2) Q' | 9.
 Proof.
   rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
-  rewrite {1}(affinely_persistently_sep_dup R). solve_sep_entails.
+  rewrite {1}(intuitionistically_sep_dup R). solve_sep_entails.
 Qed.
 Global Instance frame_sep_l R P1 P2 Q Q' :
   Frame false R P1 Q â†’ MakeSep Q P2 Q' â†’ Frame false R (P1 âˆ— P2) Q' | 9.
@@ -923,7 +931,7 @@ Global Instance frame_affinely R P Q Q' :
   Frame true R P Q â†’ MakeAffinely Q Q' â†’ Frame true R (<affine> P) Q'.
 Proof.
   rewrite /Frame /MakeAffinely=> <- <- /=.
-  by rewrite -{1}affinely_idemp affinely_sep_2.
+  rewrite -{1}(affine_affinely (â–¡ R)%I) affinely_sep_2 //.
 Qed.
 
 Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
@@ -958,7 +966,7 @@ Global Instance frame_persistently R P Q Q' :
   Frame true R P Q â†’ MakePersistently Q Q' â†’ Frame true R (<pers> P) Q'.
 Proof.
   rewrite /Frame /MakePersistently=> <- <- /=.
-  rewrite -persistently_and_affinely_sep_l.
+  rewrite -persistently_and_intuitionistically_sep_l.
   by rewrite -persistently_sep_2 -persistently_and_sep_l_1 persistently_affinely
               persistently_idemp.
 Qed.
@@ -974,16 +982,16 @@ Global Instance frame_impl_persistent R P1 P2 Q2 :
   Frame true R P2 Q2 â†’ Frame true R (P1 â†’ P2) (P1 â†’ Q2).
 Proof.
   rewrite /Frame /= => ?. apply impl_intro_l.
-  by rewrite -persistently_and_affinely_sep_l assoc (comm _ P1) -assoc impl_elim_r
-             persistently_and_affinely_sep_l.
+  by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
+             persistently_and_intuitionistically_sep_l.
 Qed.
 Global Instance frame_impl R P1 P2 Q2 :
   Persistent P1 â†’ Absorbing P1 â†’
   Frame false R P2 Q2 â†’ Frame false R (P1 â†’ P2) (P1 â†’ Q2).
 Proof.
   rewrite /Frame /==> ???. apply impl_intro_l.
-  rewrite {1}(persistent P1) persistently_and_affinely_sep_l assoc.
-  rewrite (comm _ (â–¡ P1)%I) -assoc -persistently_and_affinely_sep_l.
+  rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
+  rewrite (comm _ (â–¡ P1)%I) -assoc -persistently_and_intuitionistically_sep_l.
   rewrite persistently_elim impl_elim_r //.
 Qed.
 
@@ -1046,13 +1054,13 @@ Global Instance from_assumption_plainly_l_true `{BiPlainly PROP} P Q :
   FromAssumption true P Q â†’ KnownLFromAssumption true (â–  P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
-  by rewrite persistently_elim plainly_elim_persistently.
+  rewrite intuitionistically_plainly_elim //.
 Qed.
 Global Instance from_assumption_plainly_l_false `{BiPlainly PROP, BiAffine PROP} P Q :
   FromAssumption true P Q â†’ KnownLFromAssumption false (â–  P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
-  by rewrite affine_affinely plainly_elim_persistently.
+  rewrite plainly_elim_persistently intuitionistically_persistently //.
 Qed.
 
 (* FromPure *)
@@ -1091,71 +1099,71 @@ Global Instance into_wand_later p q R P Q :
   IntoWand p q R P Q â†’ IntoWand p q (â–· R) (â–· P) (â–· Q).
 Proof.
   rewrite /IntoWand /= => HR.
-  by rewrite !later_affinely_persistently_if_2 -later_wand HR.
+  by rewrite !later_intuitionistically_if_2 -later_wand HR.
 Qed.
 Global Instance into_wand_later_args p q R P Q :
   IntoWand p q R P Q â†’ IntoWand' p q R (â–· P) (â–· Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !later_affinely_persistently_if_2
+  by rewrite !later_intuitionistically_if_2
              (later_intro (â–¡?p R)%I) -later_wand HR.
 Qed.
 Global Instance into_wand_laterN n p q R P Q :
   IntoWand p q R P Q â†’ IntoWand p q (â–·^n R) (â–·^n P) (â–·^n Q).
 Proof.
   rewrite /IntoWand /= => HR.
-  by rewrite !laterN_affinely_persistently_if_2 -laterN_wand HR.
+  by rewrite !laterN_intuitionistically_if_2 -laterN_wand HR.
 Qed.
 Global Instance into_wand_laterN_args n p q R P Q :
   IntoWand p q R P Q â†’ IntoWand' p q R (â–·^n P) (â–·^n Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
-  by rewrite !laterN_affinely_persistently_if_2
+  by rewrite !laterN_intuitionistically_if_2
              (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
 Qed.
 
 Global Instance into_wand_bupd `{BiBUpd PROP} p q R P Q :
   IntoWand false false R P Q â†’ IntoWand p q (|==> R) (|==> P) (|==> Q).
 Proof.
-  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
+  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
   apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
 Qed.
 Global Instance into_wand_bupd_persistent `{BiBUpd PROP} p q R P Q :
   IntoWand false q R P Q â†’ IntoWand p q (|==> R) P (|==> Q).
 Proof.
-  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
+  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
   apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
 Qed.
 Global Instance into_wand_bupd_args `{BiBUpd PROP} p q R P Q :
   IntoWand p false R P Q â†’ IntoWand' p q R (|==> P) (|==> Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => ->.
-  apply wand_intro_l. by rewrite affinely_persistently_if_elim bupd_wand_r.
+  apply wand_intro_l. by rewrite intuitionistically_if_elim bupd_wand_r.
 Qed.
 
 Global Instance into_wand_fupd `{BiFUpd PROP} E p q R P Q :
   IntoWand false false R P Q â†’
   IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
 Proof.
-  rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
+  rewrite /IntoWand /= => HR. rewrite !intuitionistically_if_elim HR.
   apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
 Qed.
 Global Instance into_wand_fupd_persistent `{BiFUpd PROP} E1 E2 p q R P Q :
   IntoWand false q R P Q â†’ IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
 Proof.
-  rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
+  rewrite /IntoWand /= => HR. rewrite intuitionistically_if_elim HR.
   apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
 Qed.
 Global Instance into_wand_fupd_args `{BiFUpd PROP} E1 E2 p q R P Q :
   IntoWand p false R P Q â†’ IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => ->.
-  apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
+  apply wand_intro_l. by rewrite intuitionistically_if_elim fupd_wand_r.
 Qed.
 
 Global Instance into_wand_plainly_true `{BiPlainly PROP} q R P Q :
   IntoWand true q R P Q â†’ IntoWand true q (â–  R) P Q.
-Proof. by rewrite /IntoWand /= persistently_plainly plainly_elim_persistently. Qed.
+Proof. rewrite /IntoWand /= intuitionistically_plainly_elim //. Qed.
 Global Instance into_wand_plainly_false `{BiPlainly PROP} q R P Q :
   Absorbing R â†’ IntoWand false q R P Q â†’ IntoWand false q (â–  R) P Q.
 Proof. intros ?. by rewrite /IntoWand plainly_elim. Qed.
@@ -1201,32 +1209,31 @@ Proof. rewrite /FromSep=> <-. by rewrite plainly_sep_2. Qed.
 Global Instance into_and_later p P Q1 Q2 :
   IntoAnd p P Q1 Q2 â†’ IntoAnd p (â–· P) (â–· Q1) (â–· Q2).
 Proof.
-  rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
-  by rewrite later_affinely_persistently_if_2 HP
-             affinely_persistently_if_elim later_and.
+  rewrite /IntoAnd=> HP. apply intuitionistically_if_intro'.
+  by rewrite later_intuitionistically_if_2 HP
+             intuitionistically_if_elim later_and.
 Qed.
 Global Instance into_and_laterN n p P Q1 Q2 :
   IntoAnd p P Q1 Q2 â†’ IntoAnd p (â–·^n P) (â–·^n Q1) (â–·^n Q2).
 Proof.
-  rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
-  by rewrite laterN_affinely_persistently_if_2 HP
-             affinely_persistently_if_elim laterN_and.
+  rewrite /IntoAnd=> HP. apply intuitionistically_if_intro'.
+  by rewrite laterN_intuitionistically_if_2 HP
+             intuitionistically_if_elim laterN_and.
 Qed.
 Global Instance into_and_except_0 p P Q1 Q2 :
   IntoAnd p P Q1 Q2 â†’ IntoAnd p (â—‡ P) (â—‡ Q1) (â—‡ Q2).
 Proof.
-  rewrite /IntoAnd=> HP. apply affinely_persistently_if_intro'.
-  by rewrite except_0_affinely_persistently_if_2 HP
-             affinely_persistently_if_elim except_0_and.
+  rewrite /IntoAnd=> HP. apply intuitionistically_if_intro'.
+  by rewrite except_0_intuitionistically_if_2 HP
+             intuitionistically_if_elim except_0_and.
 Qed.
 
 Global Instance into_and_plainly `{BiPlainly PROP} p P Q1 Q2 :
   IntoAnd p P Q1 Q2 â†’ IntoAnd p (â–  P) (â–  Q1) (â–  Q2).
 Proof.
   rewrite /IntoAnd /=. destruct p; simpl.
-  - rewrite -plainly_and persistently_plainly -plainly_persistently
-            -plainly_affinely => ->.
-    by rewrite plainly_affinely plainly_persistently persistently_plainly.
+  - rewrite -plainly_and -[(â–¡ â–  P)%I]intuitionistically_idemp intuitionistically_plainly =>->.
+    rewrite [(â–¡ (_ âˆ§ _))%I]intuitionistically_elim //.
   - intros ->. by rewrite plainly_and.
 Qed.
 
@@ -1575,14 +1582,14 @@ Global Instance frame_later p R R' P Q Q' :
   Frame p R P Q â†’ MakeLaterN 1 Q Q' â†’ Frame p R' (â–· P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
-  by rewrite later_affinely_persistently_if_2 later_sep.
+  by rewrite later_intuitionistically_if_2 later_sep.
 Qed.
 Global Instance frame_laterN p n R R' P Q Q' :
   NoBackTrack (MaybeIntoLaterN true n R' R) â†’
   Frame p R P Q â†’ MakeLaterN n Q Q' â†’ Frame p R' (â–·^n P) Q'.
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
-  by rewrite laterN_affinely_persistently_if_2 laterN_sep.
+  by rewrite laterN_intuitionistically_if_2 laterN_sep.
 Qed.
 
 Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 1b17e82c3..26afcd885 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -171,10 +171,10 @@ Proof.
   - rewrite pure_True ?left_id; last (destruct Hwf, rp; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
     destruct rp.
-    + rewrite (env_lookup_perm Î“p) //= affinely_persistently_and.
-      by rewrite and_sep_affinely_persistently -assoc.
-    + rewrite {1}affinely_persistently_sep_dup {1}(env_lookup_perm Î“p) //=.
-      by rewrite affinely_persistently_and and_elim_l -assoc.
+    + rewrite (env_lookup_perm Î“p) //= intuitionistically_and.
+      by rewrite and_sep_intuitionistically -assoc.
+    + rewrite {1}intuitionistically_sep_dup {1}(env_lookup_perm Î“p) //=.
+      by rewrite intuitionistically_and and_elim_l -assoc.
   - destruct (Î“s !! i) eqn:?; simplify_eq/=.
     rewrite pure_True ?left_id; last (destruct Hwf; constructor;
       naive_solver eauto using env_delete_wf, env_delete_fresh).
@@ -194,7 +194,7 @@ Proof.
   rewrite /envs_lookup /of_envs=>?. apply pure_elim_l=> Hwf.
   destruct Î” as [Î“p Î“s], (Î“p !! i) eqn:?; simplify_eq/=.
   - rewrite pure_True // left_id (env_lookup_perm Î“p) //=
-      affinely_persistently_and and_sep_affinely_persistently.
+      intuitionistically_and and_sep_intuitionistically.
     cancel [â–¡ P]%I. apply wand_intro_l. solve_sep_entails.
   - destruct (Î“s !! i) eqn:?; simplify_eq/=.
     rewrite (env_lookup_perm Î“s) //=. rewrite pure_True // left_id.
@@ -210,13 +210,13 @@ Lemma envs_lookup_delete_list_sound Î” Î”' rp js p Ps :
   of_envs Î” âŠ¢ â–¡?p [âˆ—] Ps âˆ— of_envs Î”'.
 Proof.
   revert Î” Î”' p Ps. induction js as [|j js IH]=> Î” Î”'' p Ps ?; simplify_eq/=.
-  { by rewrite affinely_persistently_emp left_id. }
+  { by rewrite intuitionistically_emp left_id. }
   destruct (envs_lookup_delete rp j Î”) as [[[q1 P] Î”']|] eqn:Hj; simplify_eq/=.
   apply envs_lookup_delete_Some in Hj as [Hj ->].
   destruct (envs_lookup_delete_list _ js _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
-  rewrite -affinely_persistently_if_sep_2 -assoc.
+  rewrite -intuitionistically_if_sep_2 -assoc.
   rewrite envs_lookup_sound' //; rewrite IH //.
-  repeat apply sep_mono=>//; apply affinely_persistently_if_flag_mono; by destruct q1.
+  repeat apply sep_mono=>//; apply intuitionistically_if_flag_mono; by destruct q1.
 Qed.
 
 Lemma envs_lookup_delete_list_cons Î” Î”' Î”'' rp j js p1 p2 P Ps :
@@ -251,7 +251,7 @@ Proof.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (ident_beq_reflect j i); naive_solver.
-    + by rewrite affinely_persistently_and and_sep_affinely_persistently assoc.
+    + by rewrite intuitionistically_and and_sep_intuitionistically assoc.
   - apply and_intro; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
       intros j; destruct (ident_beq_reflect j i); naive_solver.
@@ -271,7 +271,7 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       naive_solver eauto using env_app_fresh.
     + rewrite (env_app_perm _ _ Î“p') //.
-      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
+      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
       solve_sep_entails.
   - destruct (env_app Î“ Î“p) eqn:Happ,
       (env_app Î“ Î“s) as [Î“s'|] eqn:?; simplify_eq/=.
@@ -299,7 +299,7 @@ Proof.
       intros j. apply (env_app_disjoint _ _ _ j) in Happ.
       destruct (decide (i = j)); try naive_solver eauto using env_replace_fresh.
     + rewrite (env_replace_perm _ _ Î“p') //.
-      rewrite big_opL_app affinely_persistently_and and_sep_affinely_persistently.
+      rewrite big_opL_app intuitionistically_and and_sep_intuitionistically.
       solve_sep_entails.
   - destruct (env_app Î“ Î“p) eqn:Happ,
       (env_replace i Î“ Î“s) as [Î“s'|] eqn:?; simplify_eq/=.
@@ -370,11 +370,11 @@ Proof.
   apply pure_intro. destruct Hwf; constructor; simpl; auto using Enil_wf.
 Qed.
 
-Lemma env_spatial_is_nil_affinely_persistently Î” :
+Lemma env_spatial_is_nil_intuitionistically Î” :
   env_spatial_is_nil Î” = true â†’ of_envs Î” âŠ¢ â–¡ of_envs Î”.
 Proof.
   intros. unfold of_envs; destruct Î” as [? []]; simplify_eq/=.
-  rewrite !right_id {1}affinely_and_r persistently_and.
+  rewrite !right_id /bi_intuitionistically {1}affinely_and_r persistently_and.
   by rewrite persistently_affinely persistently_idemp persistently_pure.
 Qed.
 
@@ -420,10 +420,10 @@ Lemma envs_split_sound Î” d js Î”1 Î”2 :
 Proof.
   rewrite /envs_split=> ?. rewrite -(idemp bi_and (of_envs Î”)).
   rewrite {2}envs_clear_spatial_sound.
-  rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
-  rewrite -persistently_and_affinely_sep_l.
+  rewrite (env_spatial_is_nil_intuitionistically (envs_clear_spatial _)) //.
+  rewrite -persistently_and_intuitionistically_sep_l.
   rewrite (and_elim_l (<pers> _)%I)
-          persistently_and_affinely_sep_r affinely_persistently_elim.
+          persistently_and_intuitionistically_sep_r intuitionistically_elim.
   destruct (envs_split_go _ _) as [[Î”1' Î”2']|] eqn:HÎ”; [|done].
   apply envs_split_go_sound in HÎ” as ->; last first.
   { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
@@ -481,8 +481,8 @@ Proof. rewrite envs_entails_eq=> Î”1 Î”2 ? P1 P2 <- <-. by f_equiv. Qed.
 (** * Adequacy *)
 Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P â†’ P.
 Proof.
-  rewrite envs_entails_eq /of_envs /= persistently_True_emp
-          affinely_persistently_emp left_id=><-.
+  rewrite envs_entails_eq /of_envs /= intuitionistically_True_emp
+          left_id=><-.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
@@ -532,7 +532,7 @@ Lemma tac_assumption Î” Î”' i p P Q :
 Proof.
   intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
   destruct (env_spatial_is_nil Î”') eqn:?.
-  - by rewrite (env_spatial_is_nil_affinely_persistently Î”') // sep_elim_l.
+  - by rewrite (env_spatial_is_nil_intuitionistically Î”') // sep_elim_l.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
@@ -566,7 +566,7 @@ Lemma tac_false_destruct Î” i p P Q :
   envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq => ??. subst. rewrite envs_lookup_sound //; simpl.
-  by rewrite affinely_persistently_if_elim sep_elim_l False_elim.
+  by rewrite intuitionistically_if_elim sep_elim_l False_elim.
 Qed.
 
 (** * Pure *)
@@ -576,8 +576,8 @@ Lemma tac_pure_intro Î” Q Ï† af :
   env_spatial_is_nil Î” = af â†’ FromPure af Q Ï† â†’ Ï† â†’ envs_entails Î” Q.
 Proof.
   intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af.
-  - rewrite env_spatial_is_nil_affinely_persistently //=. f_equiv.
-    by apply pure_intro.
+  - rewrite env_spatial_is_nil_intuitionistically //= /bi_intuitionistically.
+    f_equiv. by apply pure_intro.
   - by apply pure_intro.
 Qed.
 
@@ -589,7 +589,7 @@ Lemma tac_pure Î” Î”' i p P Ï† Q :
 Proof.
   rewrite envs_entails_eq=> ?? HPQ HQ.
   rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
-  - rewrite (into_pure P) -persistently_and_affinely_sep_l persistently_pure.
+  - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
     by apply pure_elim_l.
   - destruct HPQ.
     + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
@@ -610,13 +610,13 @@ Lemma tac_persistent Î” Î”' i p P P' Q :
   envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
-  destruct p; simpl.
+  destruct p; simpl; rewrite /bi_intuitionistically.
   - by rewrite -(into_persistent _ P) /= wand_elim_r.
   - destruct HPQ.
     + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
               (into_persistent _ P) wand_elim_r //.
     + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
-      by rewrite -{1}absorbingly_affinely_persistently
+      by rewrite -{1}absorbingly_intuitionistically
         absorbingly_sep_l wand_elim_r HQ.
 Qed.
 
@@ -629,10 +629,10 @@ Lemma tac_impl_intro Î” Î”' i P P' Q R :
   envs_entails Î”' Q â†’ envs_entails Î” R.
 Proof.
   rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Î”) eqn:?.
-  - rewrite (env_spatial_is_nil_affinely_persistently Î”) //; simpl. apply impl_intro_l.
+  - rewrite (env_spatial_is_nil_intuitionistically Î”) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
     rewrite -(from_affinely P') -affinely_and_lr.
-    by rewrite persistently_and_affinely_sep_r affinely_persistently_elim wand_elim_r.
+    by rewrite persistently_and_intuitionistically_sep_r intuitionistically_elim wand_elim_r.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
     by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
@@ -645,7 +645,7 @@ Proof.
   rewrite /FromImpl envs_entails_eq => <- ?? <-.
   rewrite envs_app_singleton_sound //=. apply impl_intro_l.
   rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
-  by rewrite persistently_and_affinely_sep_l wand_elim_r.
+  by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
 Qed.
 Lemma tac_impl_intro_drop Î” P Q R :
   FromImpl R P Q â†’ envs_entails Î” Q â†’ envs_entails Î” R.
@@ -672,8 +672,8 @@ Proof.
   rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
             (into_persistent _ P) wand_elim_r //.
-  - rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
-    by rewrite -{1}absorbingly_affinely_persistently
+  - rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
+    by rewrite -{1}absorbingly_intuitionistically
       absorbingly_sep_l wand_elim_r HQ.
 Qed.
 Lemma tac_wand_intro_pure Î” P Ï† Q R :
@@ -714,9 +714,9 @@ Proof.
   rewrite (envs_lookup_sound' _ false) //; simpl. destruct p; simpl.
   - move: Hj; rewrite envs_delete_persistent=> Hj.
     rewrite envs_simple_replace_singleton_sound //; simpl.
-    rewrite -affinely_persistently_if_idemp -affinely_persistently_idemp into_wand /=.
-    rewrite assoc (affinely_persistently_affinely_persistently_if q).
-    by rewrite affinely_persistently_if_sep_2 wand_elim_r wand_elim_r.
+    rewrite -intuitionistically_if_idemp -intuitionistically_idemp into_wand /=.
+    rewrite assoc (intuitionistically_intuitionistically_if q).
+    by rewrite intuitionistically_if_sep_2 wand_elim_r wand_elim_r.
   - move: Hj Hj'; rewrite envs_delete_spatial=> Hj Hj'.
     rewrite envs_lookup_sound // (envs_replace_singleton_sound' _ Î”'') //; simpl.
     by rewrite into_wand /= assoc wand_elim_r wand_elim_r.
@@ -768,7 +768,7 @@ Lemma tac_specialize_assert_pure Î” Î”' j q R P1 P2 Ï† Q :
   Ï† â†’ envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
-  rewrite -affinely_persistently_if_idemp into_wand /= -(from_pure _ P1).
+  rewrite -intuitionistically_if_idemp into_wand /= -(from_pure _ P1) /bi_intuitionistically.
   rewrite pure_True //= persistently_affinely persistently_pure
           affinely_True_emp affinely_emp.
   by rewrite emp_wand wand_elim_r.
@@ -787,10 +787,10 @@ Proof.
   rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
   rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
   rewrite {1}HP1 (into_absorbingly P1') (persistent_persistently_2 P1).
-  rewrite absorbingly_persistently persistently_and_affinely_sep_l assoc.
-  rewrite -affinely_persistently_if_idemp -affinely_persistently_idemp.
-  rewrite (affinely_persistently_affinely_persistently_if q).
-  by rewrite affinely_persistently_if_sep_2 into_wand wand_elim_l wand_elim_r.
+  rewrite absorbingly_persistently persistently_and_intuitionistically_sep_l assoc.
+  rewrite -intuitionistically_if_idemp -intuitionistically_idemp.
+  rewrite (intuitionistically_intuitionistically_if q).
+  by rewrite intuitionistically_if_sep_2 into_wand wand_elim_l wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent_helper Î” Î”'' j q P R R' Q :
@@ -804,9 +804,9 @@ Proof.
   rewrite envs_entails_eq => ? HR ? Hpos ? <-. rewrite -(idemp bi_and (of_envs Î”)) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
   - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
-      absorbingly_persistently sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
+      absorbingly_persistently sep_elim_r persistently_and_intuitionistically_sep_l wand_elim_r.
   - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
-       (into_persistent _ R) sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
+       (into_persistent _ R) sep_elim_r persistently_and_intuitionistically_sep_l wand_elim_r.
 Qed.
 
 (* A special version of [tac_assumption] that does not do any of the
@@ -816,7 +816,7 @@ Lemma tac_specialize_persistent_helper_done Î” i q P :
   envs_entails Î” (<absorb> P).
 Proof.
   rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
-  rewrite affinely_persistently_if_elim comm. f_equiv; auto.
+  rewrite intuitionistically_if_elim comm. f_equiv; auto.
 Qed.
 
 Lemma tac_revert Î” Î”' i p P Q :
@@ -846,9 +846,9 @@ Lemma tac_revert_ih Î” P Q {Ï† : Prop} (HÏ† : Ï†) :
   envs_entails Î” Q.
 Proof.
   rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
-  rewrite (env_spatial_is_nil_affinely_persistently Î”) //.
+  rewrite (env_spatial_is_nil_intuitionistically Î”) //.
   rewrite -(idemp bi_and (â–¡ (of_envs Î”))%I) {1}HP // HPQ.
-  by rewrite -{1}persistently_idemp !affinely_persistently_elim impl_elim_r.
+  rewrite {1}intuitionistically_persistently_1 intuitionistically_elim impl_elim_r //.
 Qed.
 
 Lemma tac_assert Î” Î”' j P Q :
@@ -856,7 +856,7 @@ Lemma tac_assert Î” Î”' j P Q :
   envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq=> ? <-. rewrite (envs_app_singleton_sound Î”) //; simpl.
-  by rewrite -(entails_wand P) // affinely_persistently_emp emp_wand.
+  by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof Î” Î”' j P Q :
@@ -865,7 +865,7 @@ Lemma tac_pose_proof Î” Î”' j P Q :
   envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq => HP ? <-. rewrite envs_app_singleton_sound //=.
-  by rewrite -HP /= affinely_persistently_emp emp_wand.
+  by rewrite -HP /= intuitionistically_emp emp_wand.
 Qed.
 
 Lemma tac_pose_proof_hyp Î” Î”' Î”'' i p j P Q :
@@ -970,7 +970,7 @@ Lemma tac_frame_pure Î” (Ï† : Prop) P Q :
   Ï† â†’ Frame true âŒœÏ†âŒ P Q â†’ envs_entails Î” Q â†’ envs_entails Î” P.
 Proof.
   rewrite envs_entails_eq => ?? ->. rewrite -(frame âŒœÏ†âŒ P) /=.
-  rewrite -persistently_and_affinely_sep_l persistently_pure.
+  rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
   auto using and_intro, pure_intro.
 Qed.
 
@@ -1002,7 +1002,7 @@ Lemma tac_or_destruct Î” Î”1 Î”2 i p j1 j2 P P1 P2 Q :
   envs_entails Î”1 Q â†’ envs_entails Î”2 Q â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq. intros ???? HP1 HP2. rewrite envs_lookup_sound //.
-  rewrite (into_or P) affinely_persistently_if_or sep_or_r; apply or_elim.
+  rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_singleton_sound' _ Î”1) //.
     by rewrite wand_elim_r.
   - rewrite (envs_simple_replace_singleton_sound' _ Î”2) //.
@@ -1048,7 +1048,7 @@ Lemma tac_exist_destruct {A} Î” i p j P (Î¦ : A â†’ PROP) Q :
   envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq => ?? HÎ¦. rewrite envs_lookup_sound //.
-  rewrite (into_exist P) affinely_persistently_if_exist sep_exist_r.
+  rewrite (into_exist P) intuitionistically_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HÎ¦ a) as (Î”'&?&?).
   rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
 Qed.
@@ -1062,7 +1062,7 @@ Lemma tac_modal_elim Î” Î”' i p Ï† P' P Q Q' :
   envs_entails Î”' Q' â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq => ???? HÎ”. rewrite envs_replace_singleton_sound //=.
-  rewrite HÎ” affinely_persistently_if_elim. by eapply elim_modal.
+  rewrite HÎ” intuitionistically_if_elim. by eapply elim_modal.
 Qed.
 
 (** * Invariants *)
@@ -1078,7 +1078,7 @@ Proof.
   rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Î”'' [? <-]].
   rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
   apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
-  rewrite affinely_persistently_if_elim -assoc wand_curry. auto.
+  rewrite intuitionistically_if_elim -assoc wand_curry. auto.
 Qed.
 
 (** * Accumulate hypotheses *)
@@ -1218,8 +1218,7 @@ Section tac_modal_intro.
   Global Instance transform_persistent_env_nil C : TransformPersistentEnv M C Enil Enil.
   Proof.
     split; [|eauto using Enil_wf|done]=> /= ??.
-    rewrite !persistently_pure !affinely_True_emp.
-    by rewrite !affinely_emp -modality_emp.
+    rewrite !intuitionistically_True_emp -modality_emp //.
   Qed.
   Global Instance transform_persistent_env_snoc (C : PROP2 â†’ PROP1 â†’ Prop) Î“ Î“' i P Q :
     C P Q â†’
@@ -1227,8 +1226,8 @@ Section tac_modal_intro.
     TransformPersistentEnv M C (Esnoc Î“ i P) (Esnoc Î“' i Q).
   Proof.
     intros ? [HÎ“ Hwf Hdom]; split; simpl.
-    - intros HC Hand. rewrite affinely_persistently_and HC // HÎ“ //.
-      by rewrite Hand -affinely_persistently_and.
+    - intros HC Hand. rewrite intuitionistically_and HC // HÎ“ //.
+      by rewrite Hand -intuitionistically_and.
     - inversion 1; constructor; auto.
     - intros j. destruct (ident_beq _ _); naive_solver.
   Qed.
@@ -1278,7 +1277,7 @@ Section tac_modal_intro.
   (** The actual introduction tactic *)
   Lemma tac_modal_intro {A} (sel : A) Î“p Î“s n Î“p' Î“s' Q Q' fi :
     FromModal M sel Q' Q â†’
-    IntoModalPersistentEnv M Î“p Î“p' (modality_persistent_spec M) â†’
+    IntoModalPersistentEnv M Î“p Î“p' (modality_intuitionistic_spec M) â†’
     IntoModalSpatialEnv M Î“s Î“s' (modality_spatial_spec M) fi â†’
     (if fi then Absorbing Q' else TCTrue) â†’
     envs_entails (Envs Î“p' Î“s' n) Q â†’ envs_entails (Envs Î“p Î“s n) Q'.
@@ -1294,16 +1293,16 @@ Section tac_modal_intro.
         { destruct HÎ“s as [| |?????? []| |]; eauto. }
         naive_solver. }
     assert (â–¡ [âˆ§] Î“p âŠ¢ M (â–¡ [âˆ§] Î“p'))%I as HMp.
-    { remember (modality_persistent_spec M).
+    { remember (modality_intuitionistic_spec M).
       destruct HÎ“p as [?|M C Î“p ?%TCForall_Forall|? M C Î“p Î“p' []|? M Î“p|M Î“p]; simpl.
-      - by rewrite {1}affinely_elim_emp (modality_emp M)
-          persistently_True_emp affinely_persistently_emp.
-      - eauto using modality_persistent_forall_big_and.
-      - eauto using modality_persistent_transform,
+      - rewrite {1}intuitionistically_elim_emp (modality_emp M)
+          intuitionistically_True_emp //.
+      - eauto using modality_intuitionistic_forall_big_and.
+      - eauto using modality_intuitionistic_transform,
           modality_and_transform.
-      - by rewrite {1}affinely_elim_emp (modality_emp M)
-          persistently_True_emp affinely_persistently_emp.
-      - eauto using modality_persistent_id. }
+      - by rewrite {1}intuitionistically_elim_emp (modality_emp M)
+          intuitionistically_True_emp.
+      - eauto using modality_intuitionistic_id. }
     move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
     remember (modality_spatial_spec M).
     destruct HÎ“s as [?|M C Î“s ?%TCForall_Forall|? M C Î“s Î“s' fi []|? M Î“s|M Î“s]; simpl.
@@ -1341,7 +1340,7 @@ Lemma tac_rewrite Î” i p Pxy d Q :
 Proof.
   intros ? A x y ? HPxy -> ?. rewrite envs_entails_eq.
   apply internal_eq_rewrite'; auto. rewrite {1}envs_lookup_sound //.
-  rewrite (into_internal_eq Pxy x y) affinely_persistently_if_elim sep_elim_l.
+  rewrite (into_internal_eq Pxy x y) intuitionistically_if_elim sep_elim_l.
   destruct d; auto using internal_eq_sym.
 Qed.
 
@@ -1359,7 +1358,7 @@ Proof.
   rewrite envs_entails_eq /IntoInternalEq => ?? A Î”' x y Î¦ HPxy HP ?? <-.
   rewrite -(idemp bi_and (of_envs Î”)) {2}(envs_lookup_sound _ i) //.
   rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
-  rewrite HP HPxy (affinely_persistently_if_elim _ (_ â‰¡ _)%I) sep_elim_l.
+  rewrite HP HPxy (intuitionistically_if_elim _ (_ â‰¡ _)%I) sep_elim_l.
   rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
   rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
   - apply (internal_eq_rewrite x y (Î» y, â–¡?q Î¦ y -âˆ— of_envs Î”')%I). solve_proper.
@@ -1392,7 +1391,7 @@ Proof.
   rewrite -{1}laterN_intro. apply and_mono, sep_mono.
   - apply pure_mono; destruct 1; constructor; naive_solver.
   - apply Hp; rewrite /= /MaybeIntoLaterN.
-    + intros P Q ->. by rewrite laterN_affinely_persistently_2.
+    + intros P Q ->. by rewrite laterN_intuitionistically_2.
     + intros P Q. by rewrite laterN_and.
   - by rewrite Hs //= right_id.
 Qed.
@@ -1403,11 +1402,11 @@ Lemma tac_lÃ¶b Î” Î”' i Q :
   envs_entails Î”' Q â†’ envs_entails Î” Q.
 Proof.
   rewrite envs_entails_eq => ?? HQ.
-  rewrite (env_spatial_is_nil_affinely_persistently Î”) //.
+  rewrite (env_spatial_is_nil_intuitionistically Î”) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
   rewrite -(lÃ¶b (<pers> Q)%I) later_persistently. apply impl_intro_l.
   rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
-  rewrite persistently_and_affinely_sep_l -{1}affinely_persistently_idemp.
-  by rewrite affinely_persistently_sep_2 wand_elim_r affinely_elim.
+  rewrite persistently_and_intuitionistically_sep_l -{1}intuitionistically_idemp.
+  rewrite intuitionistically_sep_2 wand_elim_r intuitionistically_persistently_1 //.
 Qed.
 End sbi_tactics.
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index 814d93b99..38ccec446 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -6,8 +6,8 @@ Import bi.
 (** The `iModIntro` tactic is not tied the Iris modalities, but can be
 instantiated with a variety of modalities.
 
-In order to plug in a modality, one has to decide for both the persistent and
-spatial what action should be performed upon introducing the modality:
+In order to plug in a modality, one has to decide for both the intuitionistic and
+spatial context what action should be performed upon introducing the modality:
 
 - Introduction is only allowed when the context is empty.
 - Introduction is only allowed when all hypotheses satisfy some predicate
@@ -35,7 +35,7 @@ Arguments MIEnvId {_}.
 
 Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
 
-Definition modality_intro_spec_persistent {PROP1 PROP2}
+Definition modality_intro_spec_intuitionistic {PROP1 PROP2}
     (s : modality_intro_spec PROP1 PROP2) : (PROP1 â†’ PROP2) â†’ Prop :=
   match s with
   | MIEnvIsEmpty => Î» M, True
@@ -63,7 +63,7 @@ Definition modality_intro_spec_spatial {PROP1 PROP2}
 should satisfy to justify the given actions for both contexts: *)
 Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 â†’ PROP2)
     (pspec sspec : modality_intro_spec PROP1 PROP2) := {
-  modality_mixin_persistent : modality_intro_spec_persistent pspec M;
+  modality_mixin_intuitionistic : modality_intro_spec_intuitionistic pspec M;
   modality_mixin_spatial : modality_intro_spec_spatial sspec M;
   modality_mixin_emp : emp âŠ¢ M emp;
   modality_mixin_mono P Q : (P âŠ¢ Q) â†’ M P âŠ¢ M Q;
@@ -72,23 +72,23 @@ Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 â†’ PROP2)
 
 Record modality (PROP1 PROP2 : bi) := Modality {
   modality_car :> PROP1 â†’ PROP2;
-  modality_persistent_spec : modality_intro_spec PROP1 PROP2;
+  modality_intuitionistic_spec : modality_intro_spec PROP1 PROP2;
   modality_spatial_spec : modality_intro_spec PROP1 PROP2;
   modality_mixin_of :
-    modality_mixin modality_car modality_persistent_spec modality_spatial_spec
+    modality_mixin modality_car modality_intuitionistic_spec modality_spatial_spec
 }.
 Arguments Modality {_ _} _ {_ _} _.
-Arguments modality_persistent_spec {_ _} _.
+Arguments modality_intuitionistic_spec {_ _} _.
 Arguments modality_spatial_spec {_ _} _.
 
 Section modality.
   Context {PROP1 PROP2} (M : modality PROP1 PROP2).
 
-  Lemma modality_persistent_transform C P Q :
-    modality_persistent_spec M = MIEnvTransform C â†’ C P Q â†’ â–¡ P âŠ¢ M (â–¡ Q).
+  Lemma modality_intuitionistic_transform C P Q :
+    modality_intuitionistic_spec M = MIEnvTransform C â†’ C P Q â†’ â–¡ P âŠ¢ M (â–¡ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_and_transform C P Q :
-    modality_persistent_spec M = MIEnvTransform C â†’ M P âˆ§ M Q âŠ¢ M (P âˆ§ Q).
+    modality_intuitionistic_spec M = MIEnvTransform C â†’ M P âˆ§ M Q âŠ¢ M (P âˆ§ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_spatial_transform C P Q :
     modality_spatial_spec M = MIEnvTransform C â†’ C P Q â†’ P âŠ¢ M Q.
@@ -114,14 +114,14 @@ End modality.
 Section modality1.
   Context {PROP} (M : modality PROP PROP).
 
-  Lemma modality_persistent_forall C P :
-    modality_persistent_spec M = MIEnvForall C â†’ C P â†’ â–¡ P âŠ¢ M (â–¡ P).
+  Lemma modality_intuitionistic_forall C P :
+    modality_intuitionistic_spec M = MIEnvForall C â†’ C P â†’ â–¡ P âŠ¢ M (â–¡ P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_and_forall C P Q :
-    modality_persistent_spec M = MIEnvForall C â†’ M P âˆ§ M Q âŠ¢ M (P âˆ§ Q).
+    modality_intuitionistic_spec M = MIEnvForall C â†’ M P âˆ§ M Q âŠ¢ M (P âˆ§ Q).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma modality_persistent_id P :
-    modality_persistent_spec M = MIEnvId â†’ â–¡ P âŠ¢ M (â–¡ P).
+  Lemma modality_intuitionistic_id P :
+    modality_intuitionistic_spec M = MIEnvId â†’ â–¡ P âŠ¢ M (â–¡ P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma modality_spatial_forall C P :
     modality_spatial_spec M = MIEnvForall C â†’ C P â†’ P âŠ¢ M P.
@@ -130,14 +130,14 @@ Section modality1.
     modality_spatial_spec M = MIEnvId â†’ P âŠ¢ M P.
   Proof. destruct M as [??? []]; naive_solver. Qed.
 
-  Lemma modality_persistent_forall_big_and C Ps :
-    modality_persistent_spec M = MIEnvForall C â†’
+  Lemma modality_intuitionistic_forall_big_and C Ps :
+    modality_intuitionistic_spec M = MIEnvForall C â†’
     Forall C Ps â†’ â–¡ [âˆ§] Ps âŠ¢ M (â–¡ [âˆ§] Ps).
   Proof.
     induction 2 as [|P Ps ? _ IH]; simpl.
-    - by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
-    - rewrite affinely_persistently_and -modality_and_forall // -IH.
-      by rewrite {1}(modality_persistent_forall _ P).
+    - by rewrite intuitionistically_True_emp -modality_emp.
+    - rewrite intuitionistically_and -modality_and_forall // -IH.
+      by rewrite {1}(modality_intuitionistic_forall _ P).
   Qed.
   Lemma modality_spatial_forall_big_sep C Ps :
     modality_spatial_spec M = MIEnvForall C â†’
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index af0e205e4..b780300aa 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -24,15 +24,15 @@ Section bi_modalities.
   Definition modality_affinely :=
     Modality _ modality_affinely_mixin.
 
-  Lemma modality_affinely_persistently_mixin :
+  Lemma modality_intuitionistically_mixin :
     modality_mixin (Î» P : PROP, â–¡ P)%I MIEnvId MIEnvIsEmpty.
   Proof.
-    split; simpl; eauto using equiv_entails_sym, affinely_persistently_emp,
-      affinely_mono, persistently_mono, affinely_persistently_idemp,
-      affinely_persistently_sep_2 with typeclass_instances.
+    split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
+      affinely_mono, persistently_mono, intuitionistically_idemp,
+      intuitionistically_sep_2 with typeclass_instances.
   Qed.
-  Definition modality_affinely_persistently :=
-    Modality _ modality_affinely_persistently_mixin.
+  Definition modality_intuitionistically :=
+    Modality _ modality_intuitionistically_mixin.
 
   Lemma modality_embed_mixin `{BiEmbed PROP PROP'} :
     modality_mixin (@embed PROP PROP' _)
@@ -66,7 +66,7 @@ Section sbi_modalities.
   Proof.
     split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
       laterN_mono, laterN_and, laterN_sep with typeclass_instances.
-    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
+    rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_intuitionistically_2.
   Qed.
   Definition modality_laterN n :=
     Modality _ (modality_laterN_mixin n).
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index ba13064ec..ee833a1a4 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -62,8 +62,8 @@ Proof.
   rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
 Qed.
 Global Instance from_modal_affinely_persistently_monPred_at `(sel : A) P Q ð“  i :
-  FromModal modality_affinely_persistently sel P Q â†’ MakeMonPredAt i Q ð“  â†’
-  FromModal modality_affinely_persistently sel (P i) ð“  | 0.
+  FromModal modality_intuitionistically sel P Q â†’ MakeMonPredAt i Q ð“  â†’
+  FromModal modality_intuitionistically sel (P i) ð“  | 0.
 Proof.
   rewrite /FromModal /MakeMonPredAt /==> <- <-.
   by rewrite monPred_at_affinely monPred_at_persistently.
@@ -126,13 +126,13 @@ Global Instance from_assumption_make_monPred_at_l p i j P ð“Ÿ :
   MakeMonPredAt i P ð“Ÿ â†’ IsBiIndexRel j i â†’ KnownLFromAssumption p (P j) ð“Ÿ.
 Proof.
   rewrite /MakeMonPredAt /KnownLFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
-  apply  bi.affinely_persistently_if_elim.
+  apply  bi.intuitionistically_if_elim.
 Qed.
 Global Instance from_assumption_make_monPred_at_r p i j P ð“Ÿ :
   MakeMonPredAt i P ð“Ÿ â†’ IsBiIndexRel i j â†’ KnownRFromAssumption p ð“Ÿ (P j).
 Proof.
   rewrite /MakeMonPredAt /KnownRFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
-  apply  bi.affinely_persistently_if_elim.
+  apply  bi.intuitionistically_if_elim.
 Qed.
 
 Global Instance from_assumption_make_monPred_objectively P Q :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 355154bec..13d3e4474 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1981,6 +1981,7 @@ Hint Extern 1 (envs_entails _ (â–· _)) => iNext.
 Hint Extern 1 (envs_entails _ (â–  _)) => iAlways.
 Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways.
 Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways.
+Hint Extern 1 (envs_entails _ (â–¡ _)) => iAlways.
 Hint Extern 1 (envs_entails _ (âˆƒ _, _)) => iExists _.
 Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
 Hint Extern 1 (envs_entails _ (_ âˆ¨ _)) => iLeft.
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 1d4bcc5f9..4a0a99b97 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics monpred.
-From iris.base_logic Require Import base_logic lib.invariants.
 
 Section tests.
   Context {I : biIndex} {PROP : sbi}.
-- 
GitLab