diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index aeb96f07d3563853b718475c898fdbd9e29e75c7..7d1113a18e573ff79e94cbcacd70db6261bcc066 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -12,14 +12,14 @@ Implicit Types P Q : iPropG heap_lang Î£.
 Implicit Types Î¦ : val â†’ iPropG heap_lang Î£.
 Implicit Types Î” : envs (iResUR heap_lang (globalF Î£)).
 
-Global Instance sep_destruct_mapsto l q v :
-  SepDestruct false (l â†¦{q} v) (l â†¦{q/2} v) (l â†¦{q/2} v).
-Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed.
+Global Instance into_sep_mapsto l q v :
+  IntoSep false (l â†¦{q} v) (l â†¦{q/2} v) (l â†¦{q/2} v).
+Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
 
 Lemma tac_wp_alloc Î” Î”' N E j e v Î¦ :
   to_val e = Some v â†’ 
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   (âˆ€ l, âˆƒ Î”'',
     envs_app false (Esnoc Enil j (l â†¦ v)) Î”' = Some Î”'' âˆ§
     (Î”'' âŠ¢ Î¦ (LitV (LitLoc l)))) â†’
@@ -27,60 +27,60 @@ Lemma tac_wp_alloc Î” Î”' N E j e v Î¦ :
 Proof.
   intros ???? HÎ”. rewrite -wp_alloc // -always_and_sep_l.
   apply and_intro; first done.
-  rewrite strip_later_env_sound; apply later_mono, forall_intro=> l.
+  rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
   destruct (HÎ” l) as (Î”''&?&HÎ”'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HÎ”'.
 Qed.
 
 Lemma tac_wp_load Î” Î”' N E i l q v Î¦ :
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦{q} v)%I â†’
   (Î”' âŠ¢ Î¦ v) â†’
   Î” âŠ¢ WP Load (Lit (LitLoc l)) @ E {{ Î¦ }}.
 Proof.
   intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_store Î” Î”' Î”'' N E i l v e v' Î¦ :
   to_val e = Some v' â†’
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦ v)%I â†’
   envs_simple_replace i false (Esnoc Enil i (l â†¦ v')) Î”' = Some Î”'' â†’
   (Î”'' âŠ¢ Î¦ (LitV LitUnit)) â†’ Î” âŠ¢ WP Store (Lit (LitLoc l)) e @ E {{ Î¦ }}.
 Proof.
   intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_fail Î” Î”' N E i l q v e1 v1 e2 v2 Î¦ :
   to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦{q} v)%I â†’ v â‰  v1 â†’
   (Î”' âŠ¢ Î¦ (LitV (LitBool false))) â†’
   Î” âŠ¢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Î¦ }}.
 Proof.
   intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
+  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_cas_suc Î” Î”' Î”'' N E i l v e1 v1 e2 v2 Î¦ :
   to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
   (Î” âŠ¢ heap_ctx N) â†’ nclose N âŠ† E â†’
-  StripLaterEnvs Î” Î”' â†’
+  IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦ v)%I â†’ v = v1 â†’
   envs_simple_replace i false (Esnoc Enil i (l â†¦ v2)) Î”' = Some Î”'' â†’
   (Î”'' âŠ¢ Î¦ (LitV (LitBool true))) â†’ Î” âŠ¢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Î¦ }}.
 Proof.
   intros; subst.
   rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
-  rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 End heap.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index fe01f3c17fc37162a686c6762f58f717efc134da..9611f7dcf7507f97354f63ad8ae6998f1ba3dafe 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -292,19 +292,19 @@ Proof.
 Qed.
 
 (** * Basic rules *)
-Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : â–¡?p P âŠ¢ Q.
-Arguments to_assumption _ _ _ {_}.
-Global Instance to_assumption_exact p P : ToAssumption p P P.
-Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
-Global Instance to_assumption_always_l p P Q :
-  ToAssumption p P Q â†’ ToAssumption p (â–¡ P) Q.
-Proof. rewrite /ToAssumption=><-. by rewrite always_elim. Qed.
-Global Instance to_assumption_always_r P Q :
-  ToAssumption true P Q â†’ ToAssumption true P (â–¡ Q).
-Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.
+Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : â–¡?p P âŠ¢ Q.
+Arguments from_assumption _ _ _ {_}.
+Global Instance from_assumption_exact p P : FromAssumption p P P.
+Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
+Global Instance from_assumption_always_l p P Q :
+  FromAssumption p P Q â†’ FromAssumption p (â–¡ P) Q.
+Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
+Global Instance from_assumption_always_r P Q :
+  FromAssumption true P Q â†’ FromAssumption true P (â–¡ Q).
+Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
 
 Lemma tac_assumption Î” i p P Q :
-  envs_lookup i Î” = Some (p,P) â†’ ToAssumption p P Q â†’ Î” âŠ¢ Q.
+  envs_lookup i Î” = Some (p,P) â†’ FromAssumption p P Q â†’ Î” âŠ¢ Q.
 Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
 
 Lemma tac_rename Î” Î”' i j p P Q :
@@ -327,96 +327,96 @@ Lemma tac_ex_falso Î” Q : (Î” âŠ¢ False) â†’ Î” âŠ¢ Q.
 Proof. by rewrite -(False_elim Q). Qed.
 
 (** * Pure *)
-Class ToPure (P : uPred M) (Ï† : Prop) := to_pure : P âŠ£âŠ¢ â–  Ï†.
-Arguments to_pure : clear implicits.
-Global Instance to_pure_pure Ï† : ToPure (â–  Ï†) Ï†.
+Class IsPure (P : uPred M) (Ï† : Prop) := is_pure : P âŠ£âŠ¢ â–  Ï†.
+Arguments is_pure : clear implicits.
+Global Instance is_pure_pure Ï† : IsPure (â–  Ï†) Ï†.
 Proof. done. Qed.
-Global Instance to_pure_eq {A : cofeT} (a b : A) :
-  Timeless a â†’ ToPure (a â‰¡ b) (a â‰¡ b).
+Global Instance is_pure_eq {A : cofeT} (a b : A) :
+  Timeless a â†’ IsPure (a â‰¡ b) (a â‰¡ b).
 Proof. intros; red. by rewrite timeless_eq. Qed.
-Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure (âœ“ a) (âœ“ a).
+Global Instance is_pure_valid `{CMRADiscrete A} (a : A) : IsPure (âœ“ a) (âœ“ a).
 Proof. intros; red. by rewrite discrete_valid. Qed.
 
-Lemma tac_pure_intro Î” Q (Ï† : Prop) : ToPure Q Ï† â†’ Ï† â†’ Î” âŠ¢ Q.
+Lemma tac_pure_intro Î” Q (Ï† : Prop) : IsPure Q Ï† â†’ Ï† â†’ Î” âŠ¢ Q.
 Proof. intros ->. apply pure_intro. Qed.
 
 Lemma tac_pure Î” Î”' i p P Ï† Q :
-  envs_lookup_delete i Î” = Some (p, P, Î”') â†’ ToPure P Ï† â†’
+  envs_lookup_delete i Î” = Some (p, P, Î”') â†’ IsPure P Ï† â†’
   (Ï† â†’ Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
-  rewrite (to_pure P); by apply pure_elim_sep_l.
+  rewrite (is_pure P); by apply pure_elim_sep_l.
 Qed.
 
 Lemma tac_pure_revert Î” Ï† Q : (Î” âŠ¢ â–  Ï† â†’ Q) â†’ (Ï† â†’ Î” âŠ¢ Q).
 Proof. intros HÎ” ?. by rewrite HÎ” pure_equiv // left_id. Qed.
 
 (** * Later *)
-Class StripLaterR (P Q : uPred M) := strip_later_r : P âŠ¢ â–· Q.
-Arguments strip_later_r _ _ {_}.
-Class StripLaterL (P Q : uPred M) := strip_later_l : â–· Q âŠ¢ P.
-Arguments strip_later_l _ _ {_}.
-Class StripLaterEnv (Î“1 Î“2 : env (uPred M)) :=
-  strip_later_env : env_Forall2 StripLaterR Î“1 Î“2.
-Class StripLaterEnvs (Î”1 Î”2 : envs M) := {
-  strip_later_persistent: StripLaterEnv (env_persistent Î”1) (env_persistent Î”2);
-  strip_later_spatial: StripLaterEnv (env_spatial Î”1) (env_spatial Î”2)
+Class IntoLater (P Q : uPred M) := into_later : P âŠ¢ â–· Q.
+Arguments into_later _ _ {_}.
+Class FromLater (P Q : uPred M) := from_later : â–· Q âŠ¢ P.
+Arguments from_later _ _ {_}.
+Class IntoLaterEnv (Î“1 Î“2 : env (uPred M)) :=
+  into_later_env : env_Forall2 IntoLater Î“1 Î“2.
+Class IntoLaterEnvs (Î”1 Î”2 : envs M) := {
+  into_later_persistent: IntoLaterEnv (env_persistent Î”1) (env_persistent Î”2);
+  into_later_spatial: IntoLaterEnv (env_spatial Î”1) (env_spatial Î”2)
 }.
 
-Global Instance strip_later_r_fallthrough P : StripLaterR P P | 1000.
+Global Instance into_later_fallthrough P : IntoLater P P | 1000.
 Proof. apply later_intro. Qed.
-Global Instance strip_later_r_later P : StripLaterR (â–· P) P.
+Global Instance into_later_later P : IntoLater (â–· P) P.
 Proof. done. Qed.
-Global Instance strip_later_r_and P1 P2 Q1 Q2 :
-  StripLaterR P1 Q1 â†’ StripLaterR P2 Q2 â†’ StripLaterR (P1 âˆ§ P2) (Q1 âˆ§ Q2).
+Global Instance into_later_and P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 â†’ IntoLater P2 Q2 â†’ IntoLater (P1 âˆ§ P2) (Q1 âˆ§ Q2).
 Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance strip_later_r_or P1 P2 Q1 Q2 :
-  StripLaterR P1 Q1 â†’ StripLaterR P2 Q2 â†’ StripLaterR (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
+Global Instance into_later_or P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 â†’ IntoLater P2 Q2 â†’ IntoLater (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
 Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance strip_later_r_sep P1 P2 Q1 Q2 :
-  StripLaterR P1 Q1 â†’ StripLaterR P2 Q2 â†’ StripLaterR (P1 â˜… P2) (Q1 â˜… Q2).
+Global Instance into_later_sep P1 P2 Q1 Q2 :
+  IntoLater P1 Q1 â†’ IntoLater P2 Q2 â†’ IntoLater (P1 â˜… P2) (Q1 â˜… Q2).
 Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
 
-Global Instance strip_later_r_big_sepM `{Countable K} {A}
+Global Instance into_later_big_sepM `{Countable K} {A}
     (Î¦ Î¨ : K â†’ A â†’ uPred M) (m : gmap K A) :
-  (âˆ€ x k, StripLaterR (Î¦ k x) (Î¨ k x)) â†’
-  StripLaterR ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨ k x).
+  (âˆ€ x k, IntoLater (Î¦ k x) (Î¨ k x)) â†’
+  IntoLater ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨ k x).
 Proof.
-  rewrite /StripLaterR=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
+  rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
 Qed.
-Global Instance strip_later_r_big_sepS `{Countable A}
+Global Instance into_later_big_sepS `{Countable A}
     (Î¦ Î¨ : A â†’ uPred M) (X : gset A) :
-  (âˆ€ x, StripLaterR (Î¦ x) (Î¨ x)) â†’
-  StripLaterR ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨ x).
+  (âˆ€ x, IntoLater (Î¦ x) (Î¨ x)) â†’
+  IntoLater ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨ x).
 Proof.
-  rewrite /StripLaterR=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
+  rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
 Qed.
 
-Global Instance strip_later_l_later P : StripLaterL (â–· P) P.
+Global Instance from_later_later P : FromLater (â–· P) P.
 Proof. done. Qed.
-Global Instance strip_later_l_and P1 P2 Q1 Q2 :
-  StripLaterL P1 Q1 â†’ StripLaterL P2 Q2 â†’ StripLaterL (P1 âˆ§ P2) (Q1 âˆ§ Q2).
+Global Instance from_later_and P1 P2 Q1 Q2 :
+  FromLater P1 Q1 â†’ FromLater P2 Q2 â†’ FromLater (P1 âˆ§ P2) (Q1 âˆ§ Q2).
 Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance strip_later_l_or P1 P2 Q1 Q2 :
-  StripLaterL P1 Q1 â†’ StripLaterL P2 Q2 â†’ StripLaterL (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
+Global Instance from_later_or P1 P2 Q1 Q2 :
+  FromLater P1 Q1 â†’ FromLater P2 Q2 â†’ FromLater (P1 âˆ¨ P2) (Q1 âˆ¨ Q2).
 Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance strip_later_l_sep P1 P2 Q1 Q2 :
-  StripLaterL P1 Q1 â†’ StripLaterL P2 Q2 â†’ StripLaterL (P1 â˜… P2) (Q1 â˜… Q2).
+Global Instance from_later_sep P1 P2 Q1 Q2 :
+  FromLater P1 Q1 â†’ FromLater P2 Q2 â†’ FromLater (P1 â˜… P2) (Q1 â˜… Q2).
 Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
 
-Global Instance strip_later_env_nil : StripLaterEnv Enil Enil.
+Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
 Proof. constructor. Qed.
-Global Instance strip_later_env_snoc Î“1 Î“2 i P Q :
-  StripLaterEnv Î“1 Î“2 â†’ StripLaterR P Q â†’
-  StripLaterEnv (Esnoc Î“1 i P) (Esnoc Î“2 i Q).
+Global Instance into_later_env_snoc Î“1 Î“2 i P Q :
+  IntoLaterEnv Î“1 Î“2 â†’ IntoLater P Q â†’
+  IntoLaterEnv (Esnoc Î“1 i P) (Esnoc Î“2 i Q).
 Proof. by constructor. Qed.
 
-Global Instance strip_later_envs Î“p1 Î“p2 Î“s1 Î“s2 :
-  StripLaterEnv Î“p1 Î“p2 â†’ StripLaterEnv Î“s1 Î“s2 â†’
-  StripLaterEnvs (Envs Î“p1 Î“s1) (Envs Î“p2 Î“s2).
+Global Instance into_later_envs Î“p1 Î“p2 Î“s1 Î“s2 :
+  IntoLaterEnv Î“p1 Î“p2 â†’ IntoLaterEnv Î“s1 Î“s2 â†’
+  IntoLaterEnvs (Envs Î“p1 Î“s1) (Envs Î“p2 Î“s2).
 Proof. by split. Qed.
 
-Lemma strip_later_env_sound Î”1 Î”2 : StripLaterEnvs Î”1 Î”2 â†’ Î”1 âŠ¢ â–· Î”2.
+Lemma into_later_env_sound Î”1 Î”2 : IntoLaterEnvs Î”1 Î”2 â†’ Î”1 âŠ¢ â–· Î”2.
 Proof.
   intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
   repeat apply sep_mono; try apply always_mono.
@@ -427,8 +427,8 @@ Proof.
 Qed.
 
 Lemma tac_next Î” Î”' Q Q' :
-  StripLaterEnvs Î” Î”' â†’ StripLaterL Q Q' â†’ (Î”' âŠ¢ Q') â†’ Î” âŠ¢ Q.
-Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.
+  IntoLaterEnvs Î” Î”' â†’ FromLater Q Q' â†’ (Î”' âŠ¢ Q') â†’ Î” âŠ¢ Q.
+Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.
 
 Lemma tac_lÃ¶b Î” Î”' i Q :
   envs_persistent Î” = true â†’
@@ -445,24 +445,24 @@ Qed.
 Lemma tac_always_intro Î” Q : envs_persistent Î” = true â†’ (Î” âŠ¢ Q) â†’ Î” âŠ¢ â–¡ Q.
 Proof. intros. by apply: always_intro. Qed.
 
-Class ToPersistentP (P Q : uPred M) := to_persistentP : P âŠ¢ â–¡ Q.
-Arguments to_persistentP : clear implicits.
-Global Instance to_persistentP_always_trans P Q :
-  ToPersistentP P Q â†’ ToPersistentP (â–¡ P) Q | 0.
-Proof. rewrite /ToPersistentP=> ->. by rewrite always_always. Qed.
-Global Instance to_persistentP_always P : ToPersistentP (â–¡ P) P | 1.
+Class IntoPersistentP (P Q : uPred M) := into_persistentP : P âŠ¢ â–¡ Q.
+Arguments into_persistentP : clear implicits.
+Global Instance into_persistentP_always_trans P Q :
+  IntoPersistentP P Q â†’ IntoPersistentP (â–¡ P) Q | 0.
+Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
+Global Instance into_persistentP_always P : IntoPersistentP (â–¡ P) P | 1.
 Proof. done. Qed.
-Global Instance to_persistentP_persistent P :
-  PersistentP P â†’ ToPersistentP P P | 100.
+Global Instance into_persistentP_persistent P :
+  PersistentP P â†’ IntoPersistentP P P | 100.
 Proof. done. Qed.
 
 Lemma tac_persistent Î” Î”' i p P P' Q :
-  envs_lookup i Î” = Some (p, P) â†’ ToPersistentP P P' â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoPersistentP P P' â†’
   envs_replace i p true (Esnoc Enil i P') Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros ??? <-. rewrite envs_replace_sound //; simpl.
-  by rewrite right_id (to_persistentP P) always_if_always wand_elim_r.
+  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
 Qed.
 
 (** * Implication and wand *)
@@ -475,16 +475,16 @@ Proof.
   by rewrite right_id always_wand_impl always_elim HQ.
 Qed.
 Lemma tac_impl_intro_persistent Î” Î”' i P P' Q :
-  ToPersistentP P P' â†’
+  IntoPersistentP P P' â†’
   envs_app true (Esnoc Enil i P') Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ P â†’ Q.
 Proof.
   intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
-  by rewrite right_id {1}(to_persistentP P) always_and_sep_l wand_elim_r.
+  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_impl_intro_pure Î” P Ï† Q : ToPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P â†’ Q.
+Lemma tac_impl_intro_pure Î” P Ï† Q : IsPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P â†’ Q.
 Proof.
-  intros. by apply impl_intro_l; rewrite (to_pure P); apply pure_elim_l.
+  intros. by apply impl_intro_l; rewrite (is_pure P); apply pure_elim_l.
 Qed.
 
 Lemma tac_wand_intro Î” Î”' i P Q :
@@ -493,37 +493,37 @@ Proof.
   intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Î” Î”' i P P' Q :
-  ToPersistentP P P' â†’
+  IntoPersistentP P P' â†’
   envs_app true (Esnoc Enil i P') Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ P -â˜… Q.
 Proof.
   intros. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_pure Î” P Ï† Q : ToPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P -â˜… Q.
+Lemma tac_wand_intro_pure Î” P Ï† Q : IsPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P -â˜… Q.
 Proof.
-  intros. by apply wand_intro_l; rewrite (to_pure P); apply pure_elim_sep_l.
+  intros. by apply wand_intro_l; rewrite (is_pure P); apply pure_elim_sep_l.
 Qed.
 
-Class ToWand (R P Q : uPred M) := to_wand : R âŠ¢ P -â˜… Q.
-Arguments to_wand : clear implicits.
-Global Instance to_wand_wand P Q : ToWand (P -â˜… Q) P Q.
+Class IntoWand (R P Q : uPred M) := into_wand : R âŠ¢ P -â˜… Q.
+Arguments into_wand : clear implicits.
+Global Instance into_wand_wand P Q : IntoWand (P -â˜… Q) P Q.
 Proof. done. Qed.
-Global Instance to_wand_impl P Q : ToWand (P â†’ Q) P Q.
+Global Instance into_wand_impl P Q : IntoWand (P â†’ Q) P Q.
 Proof. apply impl_wand. Qed.
-Global Instance to_wand_iff_l P Q : ToWand (P â†” Q) P Q.
+Global Instance into_wand_iff_l P Q : IntoWand (P â†” Q) P Q.
 Proof. by apply and_elim_l', impl_wand. Qed.
-Global Instance to_wand_iff_r P Q : ToWand (P â†” Q) Q P.
+Global Instance into_wand_iff_r P Q : IntoWand (P â†” Q) Q P.
 Proof. apply and_elim_r', impl_wand. Qed.
-Global Instance to_wand_always R P Q : ToWand R P Q â†’ ToWand (â–¡ R) P Q.
-+Proof. rewrite /ToWand=> ->. apply always_elim. Qed.
+Global Instance into_wand_always R P Q : IntoWand R P Q â†’ IntoWand (â–¡ R) P Q.
+Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
 Lemma tac_specialize Î” Î”' Î”'' i p j q P1 P2 R Q :
   envs_lookup_delete i Î” = Some (p, P1, Î”') â†’
   envs_lookup j (if p then Î” else Î”') = Some (q, R) â†’
-  ToWand R P1 P2 â†’
+  IntoWand R P1 P2 â†’
   match p with
   | true  => envs_simple_replace j q (Esnoc Enil j P2) Î”
   | false => envs_replace j q false (Esnoc Enil j P2) Î”'
@@ -533,22 +533,22 @@ Lemma tac_specialize Î” Î”' Î”'' i p j q P1 P2 R Q :
 Proof.
   intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
-    rewrite assoc (to_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
+    rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
     by rewrite right_id wand_elim_r.
   - rewrite envs_lookup_sound //; simpl.
     rewrite envs_lookup_sound // (envs_replace_sound' _ Î”'') //; simpl.
-    by rewrite right_id assoc (to_wand R) always_if_elim wand_elim_r wand_elim_r.
+    by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
 Qed.
 
-Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
-  to_assert : R â˜… (P -â˜… Q) âŠ¢ Q.
-Global Arguments to_assert _ _ _ {_}.
-Lemma to_assert_fallthrough P Q : ToAssert P Q P.
-Proof. by rewrite /ToAssert wand_elim_r. Qed.
+Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
+  into_assert : R â˜… (P -â˜… Q) âŠ¢ Q.
+Global Arguments into_assert _ _ _ {_}.
+Lemma into_assert_fallthrough P Q : IntoAssert P Q P.
+Proof. by rewrite /IntoAssert wand_elim_r. Qed.
 
 Lemma tac_specialize_assert Î” Î”' Î”1 Î”2' j q lr js R P1 P2 P1' Q :
   envs_lookup_delete j Î” = Some (q, R, Î”') â†’
-  ToWand R P1 P2 â†’ ToAssert P1 Q P1' â†’
+  IntoWand R P1 P2 â†’ IntoAssert P1 Q P1' â†’
   ('(Î”1,Î”2) â† envs_split lr js Î”';
     Î”2' â† envs_app false (Esnoc Enil j P2) Î”2;
     Some (Î”1,Î”2')) = Some (Î”1,Î”2') â†’ (* does not preserve position of [j] *)
@@ -559,24 +559,24 @@ Proof.
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_sound Î”2) //; simpl.
-  rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
-  rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
+  rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
+  rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
   by rewrite always_if_elim assoc !wand_elim_r.
 Qed.
 
 Lemma tac_specialize_pure Î” Î”' j q R P1 P2 Ï† Q :
   envs_lookup j Î” = Some (q, R) â†’
-  ToWand R P1 P2 â†’ ToPure P1 Ï† â†’
+  IntoWand R P1 P2 â†’ IsPure P1 Ï† â†’
   envs_simple_replace j q (Esnoc Enil j P2) Î” = Some Î”' â†’
   Ï† â†’ (Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite right_id (to_wand R) (to_pure P1) pure_equiv // wand_True wand_elim_r.
+  by rewrite right_id (into_wand R) (is_pure P1) pure_equiv // wand_True wand_elim_r.
 Qed.
 
 Lemma tac_specialize_persistent Î” Î”' Î”'' j q P1 P2 R Q :
   envs_lookup_delete j Î” = Some (q, R, Î”') â†’
-  ToWand R P1 P2 â†’
+  IntoWand R P1 P2 â†’
   envs_simple_replace j q (Esnoc Enil j P2) Î” = Some Î”'' â†’
   (Î”' âŠ¢ P1) â†’ (PersistentP P1 âˆ¨ PersistentP P2) â†’
   (Î”'' âŠ¢ Q) â†’ Î” âŠ¢ Q.
@@ -586,11 +586,11 @@ Proof.
     rewrite -(idemp uPred_and (envs_delete _ _ _)).
     rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
     rewrite envs_simple_replace_sound' //; simpl.
-    rewrite right_id (to_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
+    rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
     by rewrite wand_elim_r.
   - rewrite -(idemp uPred_and Î”) {1}envs_lookup_sound //; simpl; rewrite HP1.
     rewrite envs_simple_replace_sound //; simpl.
-    rewrite (sep_elim_r _ (_ -â˜… _)) right_id (to_wand R) always_if_elim.
+    rewrite (sep_elim_r _ (_ -â˜… _)) right_id (into_wand R) always_if_elim.
     by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
 Qed.
 
@@ -610,7 +610,7 @@ Proof.
 Qed.
 
 Lemma tac_assert Î” Î”1 Î”2 Î”2' lr js j P Q R :
-  ToAssert P Q R â†’
+  IntoAssert P Q R â†’
   envs_split lr js Î” = Some (Î”1,Î”2) â†’
   envs_app false (Esnoc Enil j P) Î”2 = Some Î”2' â†’
   (Î”1 âŠ¢ R) â†’ (Î”2' âŠ¢ Q) â†’ Î” âŠ¢ Q.
@@ -630,22 +630,24 @@ Proof.
 Qed.
 
 (** Whenever posing [lem : True âŠ¢ Q] as [H] we want it to appear as [H : Q] and
-not as [H : True -â˜… Q]. The class [ToPosedProof] is used to strip off the
+not as [H : True -â˜… Q]. The class [IntoPosedProof] is used to strip off the
 [True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
 make sure it is not used while posing [lem : ?P âŠ¢ Q] with [?P] an evar. *)
-Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : (P1 âŠ¢ P2) â†’ True âŠ¢ R.
-Arguments to_pose_proof : clear implicits.
-Instance to_posed_proof_True P : ToPosedProof True P P.
-Proof. by rewrite /ToPosedProof. Qed.
-Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P -â˜… Q).
-Proof. rewrite /ToPosedProof. apply entails_wand. Qed.
+Class IntoPosedProof (P1 P2 R : uPred M) :=
+  into_pose_proof : (P1 âŠ¢ P2) â†’ True âŠ¢ R.
+Arguments into_pose_proof : clear implicits.
+Instance to_posed_proof_True P : IntoPosedProof True P P.
+Proof. by rewrite /IntoPosedProof. Qed.
+Global Instance to_posed_proof_wand P Q : IntoPosedProof P Q (P -â˜… Q).
+Proof. rewrite /IntoPosedProof. apply entails_wand. Qed.
 
 Lemma tac_pose_proof Î” Î”' j P1 P2 R Q :
-  (P1 âŠ¢ P2) â†’ ToPosedProof P1 P2 R â†’ envs_app true (Esnoc Enil j R) Î” = Some Î”' â†’
+  (P1 âŠ¢ P2) â†’ IntoPosedProof P1 P2 R â†’
+  envs_app true (Esnoc Enil j R) Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros HP ?? <-. rewrite envs_app_sound //; simpl.
-  by rewrite right_id -(to_pose_proof P1 P2 R) // always_pure wand_True.
+  by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
 Qed.
 
 Lemma tac_pose_proof_hyp Î” Î”' Î”'' i p j P Q :
@@ -661,11 +663,11 @@ Proof.
 Qed.
 
 Lemma tac_apply Î” Î”' i p R P1 P2 :
-  envs_lookup_delete i Î” = Some (p, R, Î”') â†’ ToWand R P1 P2 â†’
+  envs_lookup_delete i Î” = Some (p, R, Î”') â†’ IntoWand R P1 P2 â†’
   (Î”' âŠ¢ P1) â†’ Î” âŠ¢ P2.
 Proof.
   intros ?? HP1. rewrite envs_lookup_delete_sound' //.
-  by rewrite (to_wand R) HP1 wand_elim_l.
+  by rewrite (into_wand R) HP1 wand_elim_l.
 Qed.
 
 (** * Rewriting *)
@@ -703,71 +705,71 @@ Proof.
 Qed.
 
 (** * Conjunction splitting *)
-Class AndSplit (P Q1 Q2 : uPred M) := and_split : Q1 âˆ§ Q2 âŠ¢ P.
-Arguments and_split : clear implicits.
+Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 âˆ§ Q2 âŠ¢ P.
+Arguments from_and : clear implicits.
 
-Global Instance and_split_and P1 P2 : AndSplit (P1 âˆ§ P2) P1 P2.
+Global Instance from_and_and P1 P2 : FromAnd (P1 âˆ§ P2) P1 P2.
 Proof. done. Qed.
-Global Instance and_split_sep_persistent_l P1 P2 :
-  PersistentP P1 â†’ AndSplit (P1 â˜… P2) P1 P2.
-Proof. intros. by rewrite /AndSplit always_and_sep_l. Qed.
-Global Instance and_split_sep_persistent_r P1 P2 :
-  PersistentP P2 â†’ AndSplit (P1 â˜… P2) P1 P2.
-Proof. intros. by rewrite /AndSplit always_and_sep_r. Qed.
-Global Instance and_split_always P Q1 Q2 :
-  AndSplit P Q1 Q2 â†’ AndSplit (â–¡ P) (â–¡ Q1) (â–¡ Q2).
-Proof. rewrite /AndSplit=> <-. by rewrite always_and. Qed.
-Global Instance and_split_later P Q1 Q2 :
-  AndSplit P Q1 Q2 â†’ AndSplit (â–· P) (â–· Q1) (â–· Q2).
-Proof. rewrite /AndSplit=> <-. by rewrite later_and. Qed.
-
-Lemma tac_and_split Î” P Q1 Q2 : AndSplit P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
-Proof. intros. rewrite -(and_split P). by apply and_intro. Qed.
+Global Instance from_and_sep_persistent_l P1 P2 :
+  PersistentP P1 â†’ FromAnd (P1 â˜… P2) P1 P2.
+Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
+Global Instance from_and_sep_persistent_r P1 P2 :
+  PersistentP P2 â†’ FromAnd (P1 â˜… P2) P1 P2.
+Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
+Global Instance from_and_always P Q1 Q2 :
+  FromAnd P Q1 Q2 â†’ FromAnd (â–¡ P) (â–¡ Q1) (â–¡ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
+Global Instance from_and_later P Q1 Q2 :
+  FromAnd P Q1 Q2 â†’ FromAnd (â–· P) (â–· Q1) (â–· Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
+
+Lemma tac_and_split Î” P Q1 Q2 : FromAnd P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
+Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
-Class SepSplit (P Q1 Q2 : uPred M) := sep_split : Q1 â˜… Q2 âŠ¢ P.
-Arguments sep_split : clear implicits.
+Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 â˜… Q2 âŠ¢ P.
+Arguments from_sep : clear implicits.
 
-Global Instance sep_split_sep P1 P2 : SepSplit (P1 â˜… P2) P1 P2 | 100.
+Global Instance from_sep_sep P1 P2 : FromSep (P1 â˜… P2) P1 P2 | 100.
 Proof. done. Qed.
-Global Instance sep_split_always P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’ SepSplit (â–¡ P) (â–¡ Q1) (â–¡ Q2).
-Proof. rewrite /SepSplit=> <-. by rewrite always_sep. Qed.
-Global Instance sep_split_later P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’ SepSplit (â–· P) (â–· Q1) (â–· Q2).
-Proof. rewrite /SepSplit=> <-. by rewrite later_sep. Qed.
-
-Global Instance sep_split_ownM (a b : M) :
-  SepSplit (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
-Proof. by rewrite /SepSplit ownM_op. Qed.
-Global Instance sep_split_big_sepM
+Global Instance from_sep_always P Q1 Q2 :
+  FromSep P Q1 Q2 â†’ FromSep (â–¡ P) (â–¡ Q1) (â–¡ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
+Global Instance from_sep_later P Q1 Q2 :
+  FromSep P Q1 Q2 â†’ FromSep (â–· P) (â–· Q1) (â–· Q2).
+Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
+
+Global Instance from_sep_ownM (a b : M) :
+  FromSep (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
+Proof. by rewrite /FromSep ownM_op. Qed.
+Global Instance from_sep_big_sepM
     `{Countable K} {A} (Î¦ Î¨1 Î¨2 : K â†’ A â†’ uPred M) m :
-  (âˆ€ k x, SepSplit (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
-  SepSplit ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
+  (âˆ€ k x, FromSep (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
+  FromSep ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
     ([â˜… map] k â†¦ x âˆˆ m, Î¨1 k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨2 k x).
 Proof.
-  rewrite /SepSplit=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
+  rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
 Qed.
-Global Instance sep_split_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) X :
-  (âˆ€ x, SepSplit (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
-  SepSplit ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
+Global Instance from_sep_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) X :
+  (âˆ€ x, FromSep (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
+  FromSep ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
 Proof.
-  rewrite /SepSplit=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
+  rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
 Qed.
 
 Lemma tac_sep_split Î” Î”1 Î”2 lr js P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’
+  FromSep P Q1 Q2 â†’
   envs_split lr js Î” = Some (Î”1,Î”2) â†’
   (Î”1 âŠ¢ Q1) â†’ (Î”2 âŠ¢ Q2) â†’ Î” âŠ¢ P.
 Proof.
-  intros. rewrite envs_split_sound // -(sep_split P). by apply sep_mono.
+  intros. rewrite envs_split_sound // -(from_sep P). by apply sep_mono.
 Qed.
 
 (** * Combining *)
 Lemma tac_combine Î”1 Î”2 Î”3 Î”4 i1 p P1 i2 q P2 j P Q :
   envs_lookup_delete i1 Î”1 = Some (p,P1,Î”2) â†’
   envs_lookup_delete i2 (if p then Î”1 else Î”2) = Some (q,P2,Î”3) â†’
-  SepSplit P P1 P2 â†’
+  FromSep P P1 P2 â†’
   envs_app (p && q) (Esnoc Enil j P)
     (if q then (if p then Î”1 else Î”2) else Î”3) = Some Î”4 â†’
   (Î”4 âŠ¢ Q) â†’ Î”1 âŠ¢ Q.
@@ -776,83 +778,81 @@ Proof.
   destruct p.
   - rewrite envs_lookup_persistent_sound //. destruct q.
     + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc -always_sep (sep_split P) wand_elim_r.
+      by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
     + rewrite envs_lookup_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
+      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
   - rewrite envs_lookup_sound //; simpl. destruct q.
     + rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc always_elim (sep_split P) wand_elim_r.
+      by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
     + rewrite envs_lookup_sound // envs_app_sound //; simpl.
-      by rewrite right_id assoc (sep_split P) wand_elim_r.
+      by rewrite right_id assoc (from_sep P) wand_elim_r.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
-Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
-  sep_destruct : â–¡?p P âŠ¢ â–¡?p (Q1 â˜… Q2).
-Arguments sep_destruct : clear implicits.
-Class OpDestruct {A : cmraT} (a b1 b2 : A) :=
-  op_destruct : a â‰¡ b1 â‹… b2.
-Arguments op_destruct {_} _ _ _ {_}.
-
-Global Instance op_destruct_op {A : cmraT} (a b : A) : OpDestruct (a â‹… b) a b.
-Proof. by rewrite /OpDestruct. Qed.
-Global Instance op_destruct_persistent {A : cmraT} (a : A) :
-  Persistent a â†’ OpDestruct a a a.
+Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : â–¡?p P âŠ¢ â–¡?p (Q1 â˜… Q2).
+Arguments into_sep : clear implicits.
+Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a â‰¡ b1 â‹… b2.
+Arguments into_op {_} _ _ _ {_}.
+
+Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a â‹… b) a b.
+Proof. by rewrite /IntoOp. Qed.
+Global Instance into_op_persistent {A : cmraT} (a : A) :
+  Persistent a â†’ IntoOp a a a.
 Proof. intros; apply (persistent_dup a). Qed.
-Global Instance op_destruct_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
-  OpDestruct a b1 b2 â†’ OpDestruct a' b1' b2' â†’
-  OpDestruct (a,a') (b1,b1') (b2,b2').
+Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+  IntoOp a b1 b2 â†’ IntoOp a' b1' b2' â†’
+  IntoOp (a,a') (b1,b1') (b2,b2').
 Proof. by constructor. Qed.
-Global Instance op_destruct_Some {A : cmraT} (a : A) b1 b2 :
-  OpDestruct a b1 b2 â†’ OpDestruct (Some a) (Some b1) (Some b2).
+Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
+  IntoOp a b1 b2 â†’ IntoOp (Some a) (Some b1) (Some b2).
 Proof. by constructor. Qed.
 
-Global Instance sep_destruct_sep p P Q : SepDestruct p (P â˜… Q) P Q.
-Proof. rewrite /SepDestruct. by rewrite always_if_sep. Qed.
-Global Instance sep_destruct_ownM p (a b1 b2 : M) :
-  OpDestruct a b1 b2 â†’
-  SepDestruct p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Global Instance into_sep_sep p P Q : IntoSep p (P â˜… Q) P Q.
+Proof. rewrite /IntoSep. by rewrite always_if_sep. Qed.
+Global Instance into_sep_ownM p (a b1 b2 : M) :
+  IntoOp a b1 b2 â†’
+  IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
 Proof.
-  rewrite /OpDestruct /SepDestruct=> ->. by rewrite ownM_op always_if_sep.
+  rewrite /IntoOp /IntoSep=> ->. by rewrite ownM_op always_if_sep.
 Qed.
 
-Global Instance sep_destruct_and P Q : SepDestruct true (P âˆ§ Q) P Q.
-Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
-Global Instance sep_destruct_and_persistent_l P Q :
-  PersistentP P â†’ SepDestruct false (P âˆ§ Q) P Q.
-Proof. intros; by rewrite /SepDestruct /= always_and_sep_l. Qed.
-Global Instance sep_destruct_and_persistent_r P Q :
-  PersistentP Q â†’ SepDestruct false (P âˆ§ Q) P Q.
-Proof. intros; by rewrite /SepDestruct /= always_and_sep_r. Qed.
+Global Instance into_sep_and P Q : IntoSep true (P âˆ§ Q) P Q.
+Proof. by rewrite /IntoSep /= always_and_sep. Qed.
+Global Instance into_sep_and_persistent_l P Q :
+  PersistentP P â†’ IntoSep false (P âˆ§ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
+Global Instance into_sep_and_persistent_r P Q :
+  PersistentP Q â†’ IntoSep false (P âˆ§ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
 
-Global Instance sep_destruct_later p P Q1 Q2 :
-  SepDestruct p P Q1 Q2 â†’ SepDestruct p (â–· P) (â–· Q1) (â–· Q2).
-Proof. by rewrite /SepDestruct -later_sep !always_if_later=> ->. Qed.
+Global Instance into_sep_later p P Q1 Q2 :
+  IntoSep p P Q1 Q2 â†’ IntoSep p (â–· P) (â–· Q1) (â–· Q2).
+Proof. by rewrite /IntoSep -later_sep !always_if_later=> ->. Qed.
 
-Global Instance sep_destruct_big_sepM
+Global Instance into_sep_big_sepM
     `{Countable K} {A} (Î¦ Î¨1 Î¨2 : K â†’ A â†’ uPred M) p m :
-  (âˆ€ k x, SepDestruct p (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
-  SepDestruct p ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
+  (âˆ€ k x, IntoSep p (Î¦ k x) (Î¨1 k x) (Î¨2 k x)) â†’
+  IntoSep p ([â˜… map] k â†¦ x âˆˆ m, Î¦ k x)
     ([â˜… map] k â†¦ x âˆˆ m, Î¨1 k x) ([â˜… map] k â†¦ x âˆˆ m, Î¨2 k x).
 Proof.
-  rewrite /SepDestruct=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
+  rewrite /IntoSep=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
   by apply big_sepM_mono.
 Qed.
-Global Instance sep_destruct_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) p X :
-  (âˆ€ x, SepDestruct p (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
-  SepDestruct p ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
+Global Instance into_sep_big_sepS `{Countable A} (Î¦ Î¨1 Î¨2 : A â†’ uPred M) p X :
+  (âˆ€ x, IntoSep p (Î¦ x) (Î¨1 x) (Î¨2 x)) â†’
+  IntoSep p ([â˜… set] x âˆˆ X, Î¦ x) ([â˜… set] x âˆˆ X, Î¨1 x) ([â˜… set] x âˆˆ X, Î¨2 x).
 Proof.
-  rewrite /SepDestruct=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
+  rewrite /IntoSep=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
   by apply big_sepS_mono.
 Qed.
 
 Lemma tac_sep_destruct Î” Î”' i p j1 j2 P P1 P2 Q :
-  envs_lookup i Î” = Some (p, P) â†’ SepDestruct p P P1 P2 â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoSep p P P1 P2 â†’
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Î” = Some Î”' â†’
   (Î”' âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.
-  by rewrite (sep_destruct p P) right_id (comm uPred_sep P1) wand_elim_r.
+  by rewrite (into_sep p P) right_id (comm uPred_sep P1) wand_elim_r.
 Qed.
 
 (** * Framing *)
@@ -930,32 +930,32 @@ Proof.
 Qed.
 
 (** * Disjunction *)
-Class OrSplit (P Q1 Q2 : uPred M) := or_split : Q1 âˆ¨ Q2 âŠ¢ P.
-Arguments or_split : clear implicits.
-Global Instance or_split_or P1 P2 : OrSplit (P1 âˆ¨ P2) P1 P2.
+Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 âˆ¨ Q2 âŠ¢ P.
+Arguments from_or : clear implicits.
+Global Instance from_or_or P1 P2 : FromOr (P1 âˆ¨ P2) P1 P2.
 Proof. done. Qed.
 
-Lemma tac_or_l Î” P Q1 Q2 : OrSplit P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ Î” âŠ¢ P.
-Proof. intros. rewrite -(or_split P). by apply or_intro_l'. Qed.
-Lemma tac_or_r Î” P Q1 Q2 : OrSplit P Q1 Q2 â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
-Proof. intros. rewrite -(or_split P). by apply or_intro_r'. Qed.
+Lemma tac_or_l Î” P Q1 Q2 : FromOr P Q1 Q2 â†’ (Î” âŠ¢ Q1) â†’ Î” âŠ¢ P.
+Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
+Lemma tac_or_r Î” P Q1 Q2 : FromOr P Q1 Q2 â†’ (Î” âŠ¢ Q2) â†’ Î” âŠ¢ P.
+Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
 
-Class OrDestruct P Q1 Q2 := or_destruct : P âŠ¢ Q1 âˆ¨ Q2.
-Arguments or_destruct : clear implicits.
-Global Instance or_destruct_or P Q : OrDestruct (P âˆ¨ Q) P Q.
+Class IntoOr P Q1 Q2 := into_or : P âŠ¢ Q1 âˆ¨ Q2.
+Arguments into_or : clear implicits.
+Global Instance into_or_or P Q : IntoOr (P âˆ¨ Q) P Q.
 Proof. done. Qed.
-Global Instance or_destruct_later P Q1 Q2 :
-  OrDestruct P Q1 Q2 â†’ OrDestruct (â–· P) (â–· Q1) (â–· Q2).
-Proof. rewrite /OrDestruct=>->. by rewrite later_or. Qed.
+Global Instance into_or_later P Q1 Q2 :
+  IntoOr P Q1 Q2 â†’ IntoOr (â–· P) (â–· Q1) (â–· Q2).
+Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
 
 Lemma tac_or_destruct Î” Î”1 Î”2 i p j1 j2 P P1 P2 Q :
-  envs_lookup i Î” = Some (p, P) â†’ OrDestruct P P1 P2 â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoOr P P1 P2 â†’
   envs_simple_replace i p (Esnoc Enil j1 P1) Î” = Some Î”1 â†’
   envs_simple_replace i p (Esnoc Enil j2 P2) Î” = Some Î”2 â†’
   (Î”1 âŠ¢ Q) â†’ (Î”2 âŠ¢ Q) â†’ Î” âŠ¢ Q.
 Proof.
   intros ???? HP1 HP2. rewrite envs_lookup_sound //.
-  rewrite (or_destruct P) always_if_or sep_or_r; apply or_elim.
+  rewrite (into_or P) always_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_sound' _ Î”1) //.
     by rewrite /= right_id wand_elim_r.
   - rewrite (envs_simple_replace_sound' _ Î”2) //.
@@ -991,41 +991,40 @@ Lemma tac_forall_revert {A} Î” (Î¦ : A â†’ uPred M) :
 Proof. intros HÎ” a. by rewrite HÎ” (forall_elim a). Qed.
 
 (** * Existential *)
-Class ExistSplit {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
-  exist_split : (âˆƒ x, Î¦ x) âŠ¢ P.
-Arguments exist_split {_} _ _ {_}.
-Global Instance exist_split_exist {A} (Î¦: A â†’ uPred M): ExistSplit (âˆƒ a, Î¦ a) Î¦.
+Class FromExist {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
+  from_exist : (âˆƒ x, Î¦ x) âŠ¢ P.
+Arguments from_exist {_} _ _ {_}.
+Global Instance from_exist_exist {A} (Î¦: A â†’ uPred M): FromExist (âˆƒ a, Î¦ a) Î¦.
 Proof. done. Qed.
 
 Lemma tac_exist {A} Î” P (Î¦ : A â†’ uPred M) :
-  ExistSplit P Î¦ â†’ (âˆƒ a, Î” âŠ¢ Î¦ a) â†’ Î” âŠ¢ P.
-Proof. intros ? [a ?]. rewrite -(exist_split P). eauto using exist_intro'. Qed.
-
-Class ExistDestruct {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
-  exist_destruct : P âŠ¢ âˆƒ x, Î¦ x.
-Arguments exist_destruct {_} _ _ {_}.
-Global Instance exist_destruct_exist {A} (Î¦ : A â†’ uPred M) :
-  ExistDestruct (âˆƒ a, Î¦ a) Î¦.
+  FromExist P Î¦ â†’ (âˆƒ a, Î” âŠ¢ Î¦ a) â†’ Î” âŠ¢ P.
+Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
+
+Class IntoExist {A} (P : uPred M) (Î¦ : A â†’ uPred M) :=
+  into_exist : P âŠ¢ âˆƒ x, Î¦ x.
+Arguments into_exist {_} _ _ {_}.
+Global Instance into_exist_exist {A} (Î¦ : A â†’ uPred M) : IntoExist (âˆƒ a, Î¦ a) Î¦.
 Proof. done. Qed.
-Global Instance exist_destruct_later {A} P (Î¦ : A â†’ uPred M) :
-  ExistDestruct P Î¦ â†’ Inhabited A â†’ ExistDestruct (â–· P) (Î» a, â–· (Î¦ a))%I.
-Proof. rewrite /ExistDestruct=> HP ?. by rewrite HP later_exist. Qed.
-Global Instance exist_destruct_always {A} P (Î¦ : A â†’ uPred M) :
-  ExistDestruct P Î¦ â†’ ExistDestruct (â–¡ P) (Î» a, â–¡ (Î¦ a))%I.
-Proof. rewrite /ExistDestruct=> HP. by rewrite HP always_exist. Qed.
+Global Instance into_exist_later {A} P (Î¦ : A â†’ uPred M) :
+  IntoExist P Î¦ â†’ Inhabited A â†’ IntoExist (â–· P) (Î» a, â–· (Î¦ a))%I.
+Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
+Global Instance into_exist_always {A} P (Î¦ : A â†’ uPred M) :
+  IntoExist P Î¦ â†’ IntoExist (â–¡ P) (Î» a, â–¡ (Î¦ a))%I.
+Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
 
 Lemma tac_exist_destruct {A} Î” i p j P (Î¦ : A â†’ uPred M) Q :
-  envs_lookup i Î” = Some (p, P) â†’ ExistDestruct P Î¦ â†’
+  envs_lookup i Î” = Some (p, P) â†’ IntoExist P Î¦ â†’
   (âˆ€ a, âˆƒ Î”',
     envs_simple_replace i p (Esnoc Enil j (Î¦ a)) Î” = Some Î”' âˆ§ (Î”' âŠ¢ Q)) â†’
   Î” âŠ¢ Q.
 Proof.
   intros ?? HÎ¦. rewrite envs_lookup_sound //.
-  rewrite (exist_destruct P) always_if_exist sep_exist_r.
+  rewrite (into_exist P) always_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HÎ¦ a) as (Î”'&?&?).
   rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
 Qed.
 End tactics.
 
-Hint Extern 0 (ToPosedProof True _ _) =>
+Hint Extern 0 (IntoPosedProof True _ _) =>
   class_apply @to_posed_proof_True : typeclass_instances.
diff --git a/proofmode/ghost_ownership.v b/proofmode/ghost_ownership.v
index 87b8e0ef366fca8ff4a7e7addd186fc601bd451f..2c557444aa43cd73ce27521f0343a33329695cb7 100644
--- a/proofmode/ghost_ownership.v
+++ b/proofmode/ghost_ownership.v
@@ -6,10 +6,10 @@ Section ghost.
 Context `{inG Î› Î£ A}.
 Implicit Types a b : A.
 
-Global Instance sep_destruct_own p Î³ a b1 b2 :
-  OpDestruct a b1 b2 â†’ SepDestruct p (own Î³ a) (own Î³ b1) (own Î³ b2).
-Proof. rewrite /OpDestruct /SepDestruct => ->. by rewrite own_op. Qed.
-Global Instance sep_split_own Î³ a b :
-  SepSplit (own Î³ (a â‹… b)) (own Î³ a) (own Î³ b) | 90.
-Proof. by rewrite /SepSplit own_op. Qed.
+Global Instance into_sep_own p Î³ a b1 b2 :
+  IntoOp a b1 b2 â†’ IntoSep p (own Î³ a) (own Î³ b1) (own Î³ b2).
+Proof. rewrite /IntoOp /IntoSep => ->. by rewrite own_op. Qed.
+Global Instance from_sep_own Î³ a b :
+  FromSep (own Î³ (a â‹… b)) (own Î³ a) (own Î³ b) | 90.
+Proof. by rewrite /FromSep own_op. Qed.
 End ghost.
diff --git a/proofmode/invariants.v b/proofmode/invariants.v
index fbb6478ec5880198823c56c4bddf31b8815ee6e7..48277e7cf32e364d58b8e12a9c6656f7a9c6ccca 100644
--- a/proofmode/invariants.v
+++ b/proofmode/invariants.v
@@ -9,23 +9,23 @@ Implicit Types N : namespace.
 Implicit Types P Q R : iProp Î› Î£.
 
 Lemma tac_inv_fsa {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E N i P Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   fsaV â†’ nclose N âŠ† E â†’ (of_envs Î” âŠ¢ inv N P) â†’
   envs_app false (Esnoc Enil i (â–· P)) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa (E âˆ– nclose N) (Î» a, â–· P â˜… Î¦ a)) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ????? HÎ”'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  intros ????? HÎ”'. rewrite (is_fsa Q) -(inv_fsa fsa _ _ P) //.
   rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_app_sound //; simpl. by rewrite right_id HÎ”'.
 Qed.
 
 Lemma tac_inv_fsa_timeless {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E N i P Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   fsaV â†’ nclose N âŠ† E â†’ (of_envs Î” âŠ¢ inv N P) â†’ TimelessP P â†’
   envs_app false (Esnoc Enil i P) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa (E âˆ– nclose N) (Î» a, P â˜… Î¦ a)) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ?????? HÎ”'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
+  intros ?????? HÎ”'. rewrite (is_fsa Q) -(inv_fsa fsa _ _ P) //.
   rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
   trans (|={E âˆ– N}=> P â˜… Î”)%I; first by rewrite pvs_timeless pvs_frame_r.
   apply (fsa_strip_pvs _).
@@ -36,7 +36,7 @@ End invariants.
 
 Tactic Notation "iInvCore" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa with _ _ _ _ N H _ _;
-    [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
     |done || eauto with ndisj (* [eauto with ndisj] is slow *)
@@ -62,7 +62,7 @@ Tactic Notation "iInv" constr(N) "as" "{" simple_intropattern(x1)
 
 Tactic Notation "iInvCore>" constr(N) "as" constr(H) :=
   eapply tac_inv_fsa_timeless with _ _ _ _ N H _ _;
-    [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iInv: cannot viewshift in goal" P
     |try fast_done (* atomic *)
     |done || eauto with ndisj (* [eauto with ndisj] is slow *)
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 5085e6c50b8fbbedad7a1430c7b2f8e2d9f0fce3..86afa3f6b9fb6156a51c91eb8df1573bbe389ba2 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -7,45 +7,44 @@ Section pvs.
 Context {Î› : language} {Î£ : iFunctor}.
 Implicit Types P Q : iProp Î› Î£.
 
-Global Instance to_assumption_pvs E p P Q :
-  ToAssumption p P Q â†’ ToAssumption p P (|={E}=> Q)%I.
-Proof. rewrite /ToAssumption=>->. apply pvs_intro. Qed.
-Global Instance sep_split_pvs E P Q1 Q2 :
-  SepSplit P Q1 Q2 â†’ SepSplit (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
-Proof. rewrite /SepSplit=><-. apply pvs_sep. Qed.
+Global Instance from_assumption_pvs E p P Q :
+  FromAssumption p P Q â†’ FromAssumption p P (|={E}=> Q)%I.
+Proof. rewrite /FromAssumption=>->. apply pvs_intro. Qed.
+Global Instance from_sep_pvs E P Q1 Q2 :
+  FromSep P Q1 Q2 â†’ FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
+Proof. rewrite /FromSep=><-. apply pvs_sep. Qed.
 Global Instance or_split_pvs E1 E2 P Q1 Q2 :
-  OrSplit P Q1 Q2 â†’ OrSplit (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
-Proof. rewrite /OrSplit=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
+  FromOr P Q1 Q2 â†’ FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
+Proof. rewrite /FromOr=><-. apply or_elim; apply pvs_mono; auto with I. Qed.
 Global Instance exists_split_pvs {A} E1 E2 P (Î¦ : A â†’ iProp Î› Î£) :
-  ExistSplit P Î¦ â†’ ExistSplit (|={E1,E2}=> P) (Î» a, |={E1,E2}=> Î¦ a)%I.
+  FromExist P Î¦ â†’ FromExist (|={E1,E2}=> P) (Î» a, |={E1,E2}=> Î¦ a)%I.
 Proof.
-  rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+  rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
 Global Instance frame_pvs E1 E2 R P Q :
   Frame R P Q â†’ Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
-Global Instance to_wand_pvs E1 E2 R P Q :
-  ToWand R P Q â†’ ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
-Proof. rewrite /ToWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
+Global Instance into_wand_pvs E1 E2 R P Q :
+  IntoWand R P Q â†’ IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
 
-Class FSASplit {A} (P : iProp Î› Î£) (E : coPset)
+Class IsFSA {A} (P : iProp Î› Î£) (E : coPset)
     (fsa : FSA Î› Î£ A) (fsaV : Prop) (Î¦ : A â†’ iProp Î› Î£) := {
-  fsa_split : fsa E Î¦ âŠ£âŠ¢ P;
-  fsa_split_is_fsa :> FrameShiftAssertion fsaV fsa;
+  is_fsa : P âŠ£âŠ¢ fsa E Î¦;
+  is_fsa_is_fsa :> FrameShiftAssertion fsaV fsa;
 }.
-Global Arguments fsa_split {_} _ _ _ _ _ {_}.
-Global Instance fsa_split_pvs E P :
-  FSASplit (|={E}=> P)%I E pvs_fsa True (Î» _, P).
+Global Arguments is_fsa {_} _ _ _ _ _ {_}.
+Global Instance is_fsa_pvs E P :
+  IsFSA (|={E}=> P)%I E pvs_fsa True (Î» _, P).
 Proof. split. done. apply _. Qed.
-Global Instance fsa_split_fsa {A} (fsa : FSA Î› Î£ A) E Î¦ :
-  FrameShiftAssertion fsaV fsa â†’ FSASplit (fsa E Î¦) E fsa fsaV Î¦.
+Global Instance is_fsa_fsa {A} (fsa : FSA Î› Î£ A) E Î¦ :
+  FrameShiftAssertion fsaV fsa â†’ IsFSA (fsa E Î¦) E fsa fsaV Î¦.
 Proof. done. Qed.
 
 Global Instance to_assert_pvs {A} P Q E (fsa : FSA Î› Î£ A) fsaV Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’ ToAssert P Q (|={E}=> P).
+  IsFSA Q E fsa fsaV Î¦ â†’ IntoAssert P Q (|={E}=> P).
 Proof.
-  intros.
-  by rewrite /ToAssert pvs_frame_r wand_elim_r -(fsa_split Q) fsa_pvs_fsa.
+  intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
 Qed.
 
 Lemma tac_pvs_intro Î” E1 E2 Q : E1 = E2 â†’ (Î” âŠ¢ Q) â†’ Î” âŠ¢ |={E1,E2}=> Q.
@@ -66,11 +65,11 @@ Qed.
 
 Lemma tac_pvs_elim_fsa {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E i p P' P Q Î¦ :
   envs_lookup i Î” = Some (p, P') â†’ P' = (|={E}=> P)%I â†’
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   envs_replace i p false (Esnoc Enil i P) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa E Î¦) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ? -> ??. rewrite -(fsa_split Q) -fsa_pvs_fsa.
+  intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
   eapply tac_pvs_elim; set_solver.
 Qed.
 
@@ -85,12 +84,12 @@ Proof.
 Qed.
 
 Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Î› Î£ A) fsaV Î” Î”' E i p P Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   envs_lookup i Î” = Some (p, â–· P)%I â†’ TimelessP P â†’
   envs_simple_replace i p (Esnoc Enil i P) Î” = Some Î”' â†’
   (Î”' âŠ¢ fsa E Î¦) â†’ Î” âŠ¢ Q.
 Proof.
-  intros ????. rewrite -(fsa_split Q) -fsa_pvs_fsa.
+  intros ????. rewrite (is_fsa Q) -fsa_pvs_fsa.
   eauto using tac_pvs_timeless.
 Qed.
 End pvs.
@@ -114,7 +113,7 @@ Tactic Notation "iPvsCore" constr(H) :=
       [env_cbv; reflexivity || fail "iPvs:" H "not found"
       |let P := match goal with |- ?P = _ => P end in
        reflexivity || fail "iPvs:" H ":" P "not a pvs with the right mask"
-      |let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+      |let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
        apply _ || fail "iPvs:" P "not a pvs"
       |env_cbv; reflexivity|simpl]
   end.
@@ -170,7 +169,7 @@ Tactic Notation "iTimeless" constr(H) :=
        |env_cbv; reflexivity|simpl]
   | |- _ =>
      eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
-       [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+       [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
         apply _ || fail "iTimeless: " P "not a pvs"
        |env_cbv; reflexivity || fail "iTimeless:" H "not found"
        |let P := match goal with |- TimelessP ?P => P end in
diff --git a/proofmode/sts.v b/proofmode/sts.v
index b4817fbac06b37a265d03596ccaee0953ed03f6f..4b535fb3c5dc74ee37b52b283fd1f326212ae8f9 100644
--- a/proofmode/sts.v
+++ b/proofmode/sts.v
@@ -8,7 +8,7 @@ Context `{stsG Î› Î£ sts} (Ï† : sts.state sts â†’ iPropG Î› Î£).
 Implicit Types P Q : iPropG Î› Î£.
 
 Lemma tac_sts_fsa {A} (fsa : FSA Î› _ A) fsaV Î” E N i Î³ S T Q Î¦ :
-  FSASplit Q E fsa fsaV Î¦ â†’
+  IsFSA Q E fsa fsaV Î¦ â†’
   fsaV â†’
   envs_lookup i Î” = Some (false, sts_ownS Î³ S T) â†’
   (of_envs Î” âŠ¢ sts_ctx Î³ N Ï†) â†’ nclose N âŠ† E â†’
@@ -18,7 +18,7 @@ Lemma tac_sts_fsa {A} (fsa : FSA Î› _ A) fsaV Î” E N i Î³ S T Q Î¦ :
       â–  sts.steps (s, T) (s', T') â˜… â–· Ï† s' â˜… (sts_own Î³ s' T' -â˜… Î¦ a)))) â†’
   Î” âŠ¢ Q.
 Proof.
-  intros ????? HÎ”'. rewrite -(fsa_split Q) -(sts_fsaS Ï† fsa) //.
+  intros ????? HÎ”'. rewrite (is_fsa Q) -(sts_fsaS Ï† fsa) //.
   rewrite // -always_and_sep_l. apply and_intro; first done.
   rewrite envs_lookup_sound //; simpl; apply sep_mono_r.
   apply forall_intro=>s; apply wand_intro_l.
@@ -36,7 +36,7 @@ Tactic Notation "iSts" constr(H) "as"
   | gname => eapply tac_sts_fsa with _ _ _ _ _ _ _ H _ _ _
   | _ => fail "iSts:" H "not a string or gname"
   end;
-    [let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
+    [let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
      apply _ || fail "iSts: cannot viewshift in goal" P
     |try fast_done (* atomic *)
     |iAssumptionCore || fail "iSts:" H "not found"
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 28d0300ca1d6a1c2c7f9bda44772824d5e9dfc77..ab34269abacb2eca10904e5aa69fafed32ecbf8c 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -68,7 +68,7 @@ Tactic Notation "iClear" constr(Hs) :=
 Tactic Notation "iExact" constr(H) :=
   eapply tac_assumption with H _ _; (* (i:=H) *)
     [env_cbv; reflexivity || fail "iExact:" H "not found"
-    |let P := match goal with |- ToAssumption _ ?P _ => P end in
+    |let P := match goal with |- FromAssumption _ ?P _ => P end in
      apply _ || fail "iExact:" H ":" P "does not match goal"].
 
 Tactic Notation "iAssumptionCore" :=
@@ -88,7 +88,7 @@ Tactic Notation "iAssumption" :=
   let rec find p Î“ Q :=
     match Î“ with
     | Esnoc ?Î“ ?j ?P => first
-       [pose proof (_ : ToAssumption p P Q) as Hass;
+       [pose proof (_ : FromAssumption p P Q) as Hass;
         apply (tac_assumption _ j p P); [env_cbv; reflexivity|apply Hass]
        |find p Î“ Q]
     end in
@@ -105,20 +105,20 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
 Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_cbv; reflexivity || fail "iPersistent:" H "not found"
-    |let Q := match goal with |- ToPersistentP ?Q _ => Q end in
+    |let Q := match goal with |- IntoPersistentP ?Q _ => Q end in
      apply _ || fail "iPersistent:" H ":" Q "not persistent"
     |env_cbv; reflexivity|].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
     [env_cbv; reflexivity || fail "iPure:" H "not found"
-    |let P := match goal with |- ToPure ?P _ => P end in
+    |let P := match goal with |- IsPure ?P _ => P end in
      apply _ || fail "iPure:" H ":" P "not pure"
     |intros pat].
 
 Tactic Notation "iPureIntro" :=
   eapply tac_pure_intro;
-    [let P := match goal with |- ToPure ?P _ => P end in
+    [let P := match goal with |- IsPure ?P _ => P end in
      apply _ || fail "iPureIntro:" P "not pure"|].
 
 (** * Specialize *)
@@ -144,7 +144,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
 
 Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
   let solve_to_wand H1 :=
-    let P := match goal with |- ToWand ?P _ _ => P end in
+    let P := match goal with |- IntoWand ?P _ _ => P end in
     apply _ || fail "iSpecialize:" H1 ":" P "not an implication/wand" in
   let rec go H1 pats :=
     lazymatch pats with
@@ -154,8 +154,8 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_cbv; reflexivity || fail "iSpecialize:" H2 "not found"
          |env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
-         |let P := match goal with |- ToWand ?P ?Q _ => P end in
-          let Q := match goal with |- ToWand ?P ?Q _ => Q end in
+         |let P := match goal with |- IntoWand ?P ?Q _ => P end in
+          let Q := match goal with |- IntoWand ?P ?Q _ => Q end in
           apply _ || fail "iSpecialize: cannot instantiate" H1 ":" P "with" H2 ":" Q
          |env_cbv; reflexivity|go H1 pats]
     | SName true ?H2 :: ?pats =>
@@ -184,7 +184,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
        eapply tac_specialize_pure with _ H1 _ _ _ _ _;
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |let Q := match goal with |- ToPure ?Q _ => Q end in
+         |let Q := match goal with |- IsPure ?Q _ => Q end in
           apply _ || fail "iSpecialize:" Q "not pure"
          |env_cbv; reflexivity
          |(*goal*)
@@ -194,7 +194,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
          [env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
          |match k with
-          | GoalStd => apply to_assert_fallthrough
+          | GoalStd => apply into_assert_fallthrough
           | GoalPvs => apply _ || fail "iSpecialize: cannot generate pvs goal"
           end
          |env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
@@ -237,7 +237,7 @@ Tactic Notation "iApply" open_constr(t) :=
     [iExact H
     |eapply tac_apply with _ H _ _ _;
        [env_cbv; reflexivity || fail 1 "iApply:" H "not found"
-       |let P := match goal with |- ToWand ?P _ _ => P end in
+       |let P := match goal with |- IntoWand ?P _ _ => P end in
         apply _ || fail 1 "iApply: cannot apply" H ":" P
        |lazy beta (* reduce betas created by instantiation *)]] in
   let Htmp := iFresh in
@@ -320,17 +320,17 @@ Tactic Notation "iRevert" "{" ident(x1) ident(x2) ident(x3) ident(x4)
 (** * Disjunction *)
 Tactic Notation "iLeft" :=
   eapply tac_or_l;
-    [let P := match goal with |- OrSplit ?P _ _ => P end in
+    [let P := match goal with |- FromOr ?P _ _ => P end in
      apply _ || fail "iLeft:" P "not a disjunction"|].
 Tactic Notation "iRight" :=
   eapply tac_or_r;
-    [let P := match goal with |- OrSplit ?P _ _ => P end in
+    [let P := match goal with |- FromOr ?P _ _ => P end in
      apply _ || fail "iRight:" P "not a disjunction"|].
 
 Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iOrDestruct:" H "not found"
-    |let P := match goal with |- OrDestruct ?P _ _ => P end in
+    |let P := match goal with |- IntoOr ?P _ _ => P end in
      apply _ || fail "iOrDestruct:" H ":" P "not a disjunction"
     |env_cbv; reflexivity || fail "iOrDestruct:" H1 "not fresh"
     |env_cbv; reflexivity || fail "iOrDestruct:" H2 "not fresh"| |].
@@ -340,7 +340,7 @@ Tactic Notation "iSplit" :=
   lazymatch goal with
   | |- _ âŠ¢ _ =>
     eapply tac_and_split;
-      [let P := match goal with |- AndSplit ?P _ _ => P end in
+      [let P := match goal with |- FromAnd ?P _ _ => P end in
        apply _ || fail "iSplit:" P "not a conjunction"| |]
   | |- _ âŠ£âŠ¢ _ => apply (anti_symm (âŠ¢))
   end.
@@ -348,13 +348,13 @@ Tactic Notation "iSplit" :=
 Tactic Notation "iSplitL" constr(Hs) :=
   let Hs := words Hs in
   eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
-    [let P := match goal with |- SepSplit ?P _ _ => P end in
+    [let P := match goal with |- FromSep ?P _ _ => P end in
      apply _ || fail "iSplitL:" P "not a separating conjunction"
     |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs "not found"| |].
 Tactic Notation "iSplitR" constr(Hs) :=
   let Hs := words Hs in
   eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
-    [let P := match goal with |- SepSplit ?P _ _ => P end in
+    [let P := match goal with |- FromSep ?P _ _ => P end in
      apply _ || fail "iSplitR:" P "not a separating conjunction"
     |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs "not found"| |].
 
@@ -364,7 +364,7 @@ Tactic Notation "iSplitR" := iSplitL "".
 Local Tactic Notation "iSepDestruct" constr(H) "as" constr(H1) constr(H2) :=
   eapply tac_sep_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [env_cbv; reflexivity || fail "iSepDestruct:" H "not found"
-    |let P := match goal with |- SepDestruct _ ?P _ _ => P end in
+    |let P := match goal with |- IntoSep _ ?P _ _ => P end in
      apply _ || fail "iSepDestruct:" H ":" P "not separating destructable"
     |env_cbv; reflexivity || fail "iSepDestruct:" H1 "or" H2 " not fresh"|].
 
@@ -395,15 +395,15 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
   eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
     [env_cbv; reflexivity || fail "iCombine:" H1 "not found"
     |env_cbv; reflexivity || fail "iCombine:" H2 "not found"
-    |let P1 := match goal with |- SepSplit _ ?P1 _ => P1 end in
-     let P2 := match goal with |- SepSplit _ _ ?P2 => P2 end in
+    |let P1 := match goal with |- FromSep _ ?P1 _ => P1 end in
+     let P2 := match goal with |- FromSep _ _ ?P2 => P2 end in
      apply _ || fail "iCombine: cannot combine" H1 ":" P1 "and" H2 ":" P2
     |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
 
 (** * Existential *)
 Tactic Notation "iExists" uconstr(x1) :=
   eapply tac_exist;
-    [let P := match goal with |- ExistSplit ?P _ => P end in
+    [let P := match goal with |- FromExist ?P _ => P end in
      apply _ || fail "iExists:" P "not an existential"
     |cbv beta; eexists x1].
 
@@ -432,7 +432,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
     "as" simple_intropattern(x) constr(Hx) :=
   eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
     [env_cbv; reflexivity || fail "iExistDestruct:" H "not found"
-    |let P := match goal with |- ExistDestruct ?P _ => P end in
+    |let P := match goal with |- IntoExist ?P _ => P end in
      apply _ || fail "iExistDestruct:" H ":" P "not an existential"|];
   let y := fresh in
   intros y; eexists; split;
@@ -498,18 +498,18 @@ Tactic Notation "iAlways":=
 Tactic Notation "iNext":=
   eapply tac_next;
     [apply _
-    |let P := match goal with |- StripLaterL ?P _ => P end in
+    |let P := match goal with |- FromLater ?P _ => P end in
      apply _ || fail "iNext:" P "does not contain laters"|].
 
 (** * Introduction tactic *)
 Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" := first
   [ (* (âˆ€ _, _) *) apply tac_forall_intro; intros x
   | (* (?P â†’ _) *) eapply tac_impl_intro_pure;
-     [let P := match goal with |- ToPure ?P _ => P end in
+     [let P := match goal with |- IsPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   | (* (?P -â˜… _) *) eapply tac_wand_intro_pure;
-     [let P := match goal with |- ToPure ?P _ => P end in
+     [let P := match goal with |- IsPure ?P _ => P end in
       apply _ || fail "iIntro:" P "not pure"
      |intros x]
   |intros x].
@@ -528,12 +528,12 @@ Local Tactic Notation "iIntro" constr(H) := first
 Local Tactic Notation "iIntro" "#" constr(H) := first
   [ (* (?P â†’ _) *)
     eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- ToPersistentP ?P _ => P end in
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
        apply _ || fail 1 "iIntro: " P " not persistent"
       |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
   | (* (?P -â˜… _) *)
     eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
-      [let P := match goal with |- ToPersistentP ?P _ => P end in
+      [let P := match goal with |- IntoPersistentP ?P _ => P end in
        apply _ || fail 1 "iIntro: " P " not persistent"
       |env_cbv; reflexivity || fail 1 "iIntro:" H "not fresh"|]
   | fail 1 "iIntro: nothing to introduce" ].
@@ -746,7 +746,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
   | [SGoal ?k ?lr ?Hs] =>
      eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
        [match k with
-        | GoalStd => apply to_assert_fallthrough
+        | GoalStd => apply into_assert_fallthrough
         | GoalPvs => apply _ || fail "iAssert: cannot generate pvs goal"
         end
        |env_cbv; reflexivity || fail "iAssert:" Hs "not found"
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 2e60cd40e9d4d4b24fedff69edd140ceafa25fac..e7249a464a4880bf6186676c4dd352c7fab5566b 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -11,7 +11,7 @@ Implicit Types Î¦ : val Î› â†’ iProp Î› Î£.
 Global Instance frame_wp E e R Î¦ Î¨ :
   (âˆ€ v, Frame R (Î¦ v) (Î¨ v)) â†’ Frame R (WP e @ E {{ Î¦ }}) (WP e @ E {{ Î¨ }}).
 Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
-Global Instance fsa_split_wp E e Î¦ :
-  FSASplit (WP e @ E {{ Î¦ }})%I E (wp_fsa e) (language.atomic e) Î¦.
+Global Instance is_fsa_wp E e Î¦ :
+  IsFSA (WP e @ E {{ Î¦ }})%I E (wp_fsa e) (language.atomic e) Î¦.
 Proof. split. done. apply _. Qed.
 End weakestpre.