diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 6523f643d5d7398f4eeb5f8b5e5e9cad64bc1017..796a8557b11f1aca8fc1e9df5973cde3179b8ef5 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -112,7 +112,7 @@ Section heap.
   Implicit Types E : coPset.
 
   (** General properties of mapsto and freeable *)
-  Global Instance heap_mapsto_timeless l q v : TimelessP (l↦{q}v).
+  Global Instance heap_mapsto_timeless l q v : Timeless (l↦{q}v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
   Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
@@ -124,7 +124,7 @@ Section heap.
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. split. done. apply _. Qed.
 
-  Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
+  Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
   Proof. rewrite /heap_mapsto_vec. apply _. Qed.
 
   Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
@@ -136,7 +136,7 @@ Section heap.
     AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
   Proof. split. done. apply _. Qed.
 
-  Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
+  Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
   Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
 
   Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
@@ -219,7 +219,7 @@ Section heap.
   Qed.
 
   Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
-    (∀ vl, PersistentP (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
+    (∀ vl, Persistent (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
   Proof.
     intros p q q'. iSplit.
     - iIntros "H". iDestruct "H" as (vl) "[[Hown1 Hown2] #HP]".
@@ -242,7 +242,7 @@ Section heap.
         rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
   Qed.
   Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
-    (∀ vl, PersistentP (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
+    (∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
   Proof. split. done. apply _. Qed.
 
   Lemma inter_lookup_Some i j (n : nat):
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 10ec7bbe63547e04116f929cda07c5c16e195299..38db542c1368f32a569fbde7ba2d5151ef4aea2a 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -122,8 +122,8 @@ Section def.
   Definition weak_tok γ : iProp Σ :=
     own γ (◯ (None, 1%nat)).
 
-  Global Instance arc_tok_timeless γ q : TimelessP (arc_tok γ q) := _.
-  Global Instance weak_tok_timeless γ : TimelessP (weak_tok γ) := _.
+  Global Instance arc_tok_timeless γ q : Timeless (arc_tok γ q) := _.
+  Global Instance weak_tok_timeless γ : Timeless (weak_tok γ) := _.
 
   Definition arc_inv (γ : gname) (l : loc) : iProp Σ :=
     (∃ st : arc_stR, own γ (● st) ∗
@@ -142,7 +142,7 @@ Section def.
   Definition is_arc (γ : gname) (l : loc) : iProp Σ :=
     inv N (arc_inv γ l).
 
-  Global Instance is_arc_persistent γ l : PersistentP (is_arc γ l) := _.
+  Global Instance is_arc_persistent γ l : Persistent (is_arc γ l) := _.
 
   Definition arc_tok_acc (γ : gname) P E : iProp Σ :=
     (□ (P ={E,∅}=∗ ∃ q, arc_tok γ q ∗ (arc_tok γ q ={∅,E}=∗ P)))%I.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index d817658df83c25ee54578502e69905e1606e88fb..2a2afc167e0bd559123e7cd723748f54f0f0c0bb 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -161,7 +161,7 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
 Proof.
   intros ?? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
-  rewrite -always_and_sep_l. apply and_intro; first done.
+  rewrite -and_sep_l. apply and_intro; first done.
   rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
   apply forall_intro=>sz. apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
   apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 4148b93e8c6817f8e368232fc1ad9cc64d80877f..b9fef2cf10422a6c35895a36884cfc4eec2eca24 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -27,7 +27,7 @@ Section atomic_bors.
     iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
-  Global Instance at_bor_persistent : PersistentP (&at{κ, N} P) := _.
+  Global Instance at_bor_persistent : Persistent (&at{κ, N} P) := _.
 
   Lemma bor_share E κ :
     N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index d700003cc32b5fe38a0d9873350941e2e06db6c8..f7c31e84c93edfaf9b820963589580e1821944c3 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -34,7 +34,7 @@ Section frac_bor.
     iSplit; iIntros "H"; iDestruct "H" as (q) "[H ?]"; iExists q; iFrame; by iApply "Hφφ'".
   Qed.
 
-  Global Instance frac_bor_persistent κ : PersistentP (&frac{κ}φ) := _.
+  Global Instance frac_bor_persistent κ : Persistent (&frac{κ}φ) := _.
 
   Lemma bor_fracture E κ :
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index e5c15254f70b1af38916ca4e0a67ef4889f1fb26..a05aa8af9a649d193d536c14bd2395342dcf94cf 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -119,7 +119,7 @@ Proof.
   iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
 Qed.
 
-Lemma bor_persistent P `{!PersistentP P} E κ :
+Lemma bor_persistent P `{!Persistent P} E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
 Proof.
@@ -129,7 +129,7 @@ Proof.
   - iMod "Hclose" as "_". auto.
 Qed.
 
-Lemma bor_persistent_tok P `{!PersistentP P} E κ q :
+Lemma bor_persistent_tok P `{!Persistent P} E κ q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
 Proof.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 4ac1bd858402b4ed8313f0573cc710157c03da5a..78f08a316c71084c4a7b4e497ee24e675c617314 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -59,14 +59,14 @@ Module Type lifetime_sig.
   Global Declare Instance lft_intersect_left_id : LeftId eq static lft_intersect.
   Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect.
 
-  Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
-  Global Declare Instance lft_dead_persistent κ : PersistentP ([†κ]).
-  Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
-  Global Declare Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
-
-  Global Declare Instance lft_tok_timeless q κ : TimelessP (q.[κ]).
-  Global Declare Instance lft_dead_timeless κ : TimelessP ([†κ]).
-  Global Declare Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
+  Global Declare Instance lft_ctx_persistent : Persistent lft_ctx.
+  Global Declare Instance lft_dead_persistent κ : Persistent ([†κ]).
+  Global Declare Instance lft_incl_persistent κ κ' : Persistent (κ ⊑ κ').
+  Global Declare Instance idx_bor_persistent κ i P : Persistent (&{κ,i} P).
+
+  Global Declare Instance lft_tok_timeless q κ : Timeless (q.[κ]).
+  Global Declare Instance lft_dead_timeless κ : Timeless ([†κ]).
+  Global Declare Instance idx_bor_own_timeless q i : Timeless (idx_bor_own q i).
 
   Global Instance idx_bor_params : Params (@idx_bor) 5.
   Global Instance bor_params : Params (@bor) 4.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index fd37a3f7913483041b27cd3e4d9c849183448995..4c8c24fbb216e07f418bc658b16fe8d243e01df3 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -98,8 +98,8 @@ Proof.
     iDestruct (own_bor_valid_2 with "Hown Hbor2")
         as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
     iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
-    { iIntros (->).
-      iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
+    { iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
+      iPureIntro. iIntros (->). (* FIXME this used to work without iPureIntro. *)
       exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
       by intros [[]]. }
     iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
@@ -138,4 +138,4 @@ Proof.
       iRight. iSplit; last by auto. iExists _. iFrame. }
     unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
 Qed.
-End borrow.
\ No newline at end of file
+End borrow.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 41545ef98b54bc8f0c1e275d85cc79005c57b4a1..136adc2b37848feeff7ad20a26999ecc8a293ce9 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -320,23 +320,23 @@ Proof. solve_contractive. Qed.
 Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
 Proof. apply (ne_proper _). Qed.
 
-(*** PersistentP and TimelessP and instances  *)
-Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
+(*** Persistent and Timeless and instances  *)
+Global Instance lft_tok_timeless q κ : Timeless q.[κ].
 Proof. rewrite /lft_tok. apply _. Qed.
 
-Global Instance lft_dead_persistent κ : PersistentP [†κ].
+Global Instance lft_dead_persistent κ : Persistent [†κ].
 Proof. rewrite /lft_dead. apply _. Qed.
-Global Instance lft_dead_timeless κ : TimelessP [†κ].
+Global Instance lft_dead_timeless κ : Timeless [†κ].
 Proof. rewrite /lft_dead. apply _. Qed.
 
-Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
+Global Instance lft_incl_persistent κ κ' : Persistent (κ ⊑ κ').
 Proof. rewrite /lft_incl. apply _. Qed.
 
-Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
+Global Instance idx_bor_persistent κ i P : Persistent (&{κ,i} P).
 Proof. rewrite /idx_bor. apply _. Qed.
-Global Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
+Global Instance idx_bor_own_timeless q i : Timeless (idx_bor_own q i).
 Proof. rewrite /idx_bor_own. apply _. Qed.
 
-Global Instance lft_ctx_persistent : PersistentP lft_ctx.
+Global Instance lft_ctx_persistent : Persistent lft_ctx.
 Proof. rewrite /lft_ctx. apply _. Qed.
 End basic_properties.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 64adfc2cfaae777f01219abe30ef10a7951fe46d..e3864ebdf84cbf51ac0766356ca7bb785605303a 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -28,7 +28,7 @@ Section na_bor.
     iApply (idx_bor_iff with "HPP' HP").
   Qed.
 
-  Global Instance na_bor_persistent κ : PersistentP (&na{κ,tid,N} P) := _.
+  Global Instance na_bor_persistent κ : Persistent (&na{κ,tid,N} P) := _.
 
   Lemma bor_na κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &na{κ,tid,N}P.
   Proof.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 847cac84d96b4b11dd024a849054751ac6d5e654..fb89f3fae4059dc0e20b7a2646e7db22fe4cd40f 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -60,7 +60,7 @@ Section fixpoint.
       eapply (limit_preserving_ext (λ _, _ ∧ _)).
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
-      + apply uPred.limit_preserving_PersistentP; solve_proper.
+      + apply uPred.limit_preserving_Persistent; solve_proper.
       + apply limit_preserving_impl, uPred.limit_preserving_entails;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 4c81124ff4f7a64dffd03e0647ad9d9ac6299d56..d1506438c7736ef4783b4e5840940fb7c52b3202 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -36,7 +36,7 @@ Section lft_contexts.
     Proper ((≡ₚ) ==> (⊣⊢)) elctx_interp.
   Proof. intros ???. by apply big_opL_permutation. Qed.
   Global Instance elctx_interp_persistent E :
-    PersistentP (elctx_interp E).
+    Persistent (elctx_interp E).
   Proof. apply _. Qed.
 
   (* Local lifetime contexts. *)
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index dbc6ede2ba4b896f4a9a6f4b8638e839a8416ff5..be11f559223c9b66da68752ed0681850544e3632 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -88,7 +88,7 @@ Section rc.
               (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
               □ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]))%I.
 
-  Global Instance rc_persist_persistent : PersistentP (rc_persist tid ν γ l ty).
+  Global Instance rc_persist_persistent : Persistent (rc_persist tid ν γ l ty).
   Proof. unfold rc_persist, tc_opaque. apply _. Qed.
 
   Global Instance rc_persist_ne ν γ l n :
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 9d6b85b411d2794bd06e15ec00924d64b3bded09..d8111cdcfd376007a104d1de7db1543e08bd2148 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -17,7 +17,7 @@ Section own.
     end%I.
   Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
   Arguments freeable_sz : simpl never.
-  Global Instance freable_sz_timeless n sz l : TimelessP (freeable_sz n sz l).
+  Global Instance freable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
 
   Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ †{1}l…n ∨ ⌜Z.of_nat n = 0⌝.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 6ad1ecb4c9aeb13f5213f47413d3414a6a30abe3..107c3b0437d99613ef7ffb34ce55ba7b38bac8d6 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -178,7 +178,7 @@ Section sum.
   Proof.
     intros HFA. split.
     - intros tid vl.
-      cut (∀ i vl', PersistentP (ty_own (nth i tyl emp0) tid vl')). by apply _.
+      cut (∀ i vl', Persistent (ty_own (nth i tyl emp0) tid vl')). by apply _.
       intros. apply @copy_persistent.
       edestruct nth_in_or_default as [| ->]; [by eapply List.Forall_forall| ].
       split; first by apply _. iIntros (????????) "? []".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 73f808382d72df874328e11a006a9e6075b43307..2545c45f44ce36d667f219710eb9f0aff37141fd 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -24,7 +24,7 @@ Record type `{typeG Σ} :=
     ty_own : thread_id → list val → iProp Σ;
     ty_shr : lft → thread_id → loc → iProp Σ;
 
-    ty_shr_persistent κ tid l : PersistentP (ty_shr κ tid l);
+    ty_shr_persistent κ tid l : Persistent (ty_shr κ tid l);
 
     ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_size⌝;
     (* The mask for starting the sharing does /not/ include the
@@ -116,7 +116,7 @@ Qed.
 Record simple_type `{typeG Σ} :=
   { st_own : thread_id → list val → iProp Σ;
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
-    st_own_persistent tid vl : PersistentP (st_own tid vl) }.
+    st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2.
 
@@ -170,7 +170,7 @@ Section ofe.
     (prodC natC (thread_id -c> list val -c> iProp Σ))
     (lft -c> thread_id -c> loc -c> iProp Σ).
   Let P (x : T) : Prop :=
-    (∀ κ tid l, PersistentP (x.2 κ tid l)) ∧
+    (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
     (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
     (∀ E κ l tid q, lftE ⊆ E →
       lft_ctx -∗ &{κ} (l ↦∗: λ vs, x.1.2 tid vs) -∗
@@ -215,7 +215,7 @@ Section ofe.
     - by intros [].
     - (* TODO: automate this *)
       repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
-      + apply uPred.limit_preserving_PersistentP=> n ty1 ty2 Hty; apply Hty.
+      + apply uPred.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
       + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
       + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
       + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
@@ -390,7 +390,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
   end.
 
 Class Copy `{typeG Σ} (t : type) := {
-  copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
+  copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
   copy_shr_acc κ tid E F l q :
     lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
     lft_ctx -∗ t.(ty_shr) κ tid l -∗ na_own tid F -∗ q.[κ] ={E}=∗
@@ -545,7 +545,7 @@ Section subtyping.
     rewrite /type_incl. repeat ((by auto) || f_equiv).
   Qed.
 
-  Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
+  Global Instance type_incl_persistent ty1 ty2 : Persistent (type_incl ty1 ty2) := _.
 
   Lemma type_incl_refl ty : type_incl ty ty.
   Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 6e5ec879100b2d6da5ccc394d96333639b16df8d..aa8796768ea53dfa3d640e8a23548423e43255e0 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -135,7 +135,7 @@ Section type_context.
 
   (** Copy typing contexts *)
   Class CopyC (T : tctx) :=
-    copyc_persistent tid : PersistentP (tctx_interp tid T).
+    copyc_persistent tid : Persistent (tctx_interp tid T).
   Global Existing Instances copyc_persistent.
 
   Global Instance tctx_nil_copy : CopyC [].
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 1b907a641b09243d71b38c29790f423482ca339f..9dae5dacdfe39c5f60988421651f6c1724c55e1f 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -19,7 +19,7 @@ Section util.
      part.
 
   Lemma delay_borrow_step :
-    lfeE ⊆ N → (∀ x, PersistentP (Post x)) →
+    lfeE ⊆ N → (∀ x, Persistent (Post x)) →
     lft_ctx -∗ &{κ} P -∗
       □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x) ={N}=∗ 
       □ (∀ x, Pre x -∗ Frame x ={F1 x,F2 x}▷=∗ Post x ∗ Frame x).