diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 1e309b93563904167a6765c055c9bee0f8297c46..659e3d2833092518db5e1f5072116bcd23271b55 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
+  "coq-iris"  { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
   "coq-orc11" {= version}
 ]
 
diff --git a/gpfsl-examples/big_op.v b/gpfsl-examples/big_op.v
index 9f72e908f899e391cbfea5e88cef75b34d17bac8..11a34f4136c94d94ac1f0f360f19661c11c8c45e 100644
--- a/gpfsl-examples/big_op.v
+++ b/gpfsl-examples/big_op.v
@@ -49,12 +49,12 @@ Section big_op_map.
       ∀ x', Ψ i x' -∗
       [∗ map] k↦y ∈ <[i := x']> m, Ψ k y.
   Proof.
-    intros. rewrite big_sepM_delete //. apply sep_mono_r, forall_intro=> Ψ.
+    intros. rewrite big_sepM_delete //. apply entails_wand, sep_mono_r, forall_intro=> Ψ.
     apply wand_intro_r, forall_intro=> x'.
     apply bi.wand_intro_l.
     rewrite (big_sepM_delete Ψ (<[i:=x']>m) i x'); last by rewrite lookup_insert.
     apply sep_mono_r. rewrite delete_insert_delete.
-    eapply wand_apply; [apply big_sepM_impl|apply sep_mono_r].
+    eapply wand_apply; [apply wand_entails, big_sepM_impl|apply sep_mono_r].
     f_equiv; f_equiv=> k; f_equiv=> y.
     rewrite impl_curry -pure_and lookup_delete_Some.
     do 2 f_equiv. intros ?; naive_solver.
diff --git a/gpfsl-examples/event/ghost.v b/gpfsl-examples/event/ghost.v
index aa85f976208d7db3fe6ec883a035cec5d27b798b..b24e08e59559e52adadcb415747d2f1109c6adb3 100644
--- a/gpfsl-examples/event/ghost.v
+++ b/gpfsl-examples/event/ghost.v
@@ -90,7 +90,7 @@ Definition SeenEvent E eid eV : vProp :=
 
 (* Properties *)
 Lemma SeenLogview_union E M1 M2 :
-  SeenLogview E M1 -∗ SeenLogview E M2 -∗ SeenLogview E (M1 ∪ M2).
+  SeenLogview E M1 ⊢ SeenLogview E M2 -∗ SeenLogview E (M1 ∪ M2).
 Proof.
   constructor => ?. iIntros "P1" (V ->). iDestruct "P1" as %P1. iPureIntro.
   by apply seen_logview_union.
@@ -160,7 +160,7 @@ Lemma SeenLogview_empty E : ⊢ SeenLogview E ∅.
 Proof. rewrite SeenLogview_unfold. by iIntros (??). Qed.
 
 Lemma SeenEvent_mono E E' eid eV :
-  E ⊑ E' → SeenEvent E eid eV -∗ SeenEvent E' eid eV.
+  E ⊑ E' → SeenEvent E eid eV ⊢ SeenEvent E' eid eV.
 Proof.
   iIntros (Sub) "(% & At & $)". erewrite SeenLogview_map_mono; eauto. iFrame.
   iPureIntro. by eapply prefix_lookup_Some.
@@ -176,7 +176,7 @@ Lemma SyncLogview_SeenLogview E M :
 Proof. constructor => ?. iPureIntro. by apply sync_logview_seen_logview. Qed.
 
 Lemma SyncLogview_union E M1 M2 :
-  SyncLogview E M1 -∗ SyncLogview E M2 -∗ SyncLogview E (M1 ∪ M2).
+  SyncLogview E M1 ⊢ SyncLogview E M2 -∗ SyncLogview E (M1 ∪ M2).
 Proof.
   constructor => ?. iIntros "P1" (V ->). iDestruct "P1" as %P1. iPureIntro.
   by apply sync_logview_union.
@@ -211,7 +211,7 @@ Lemma SyncLogview_empty E : ⊢ SyncLogview E ∅.
 Proof. rewrite SyncLogview_unfold. by iIntros (??). Qed.
 
 Lemma SyncEvent_mono E E' eid eV :
-  E ⊑ E' → SyncEvent E eid eV -∗ SyncEvent E' eid eV.
+  E ⊑ E' → SyncEvent E eid eV ⊢ SyncEvent E' eid eV.
 Proof.
   iIntros (Sub) "(% & At & $)". erewrite SyncLogview_map_mono; eauto. iFrame.
   iPureIntro. by eapply prefix_lookup_Some.
diff --git a/gpfsl-examples/exchanger/proof_graph_piggyback.v b/gpfsl-examples/exchanger/proof_graph_piggyback.v
index ee9f25a7ae637febaa22245eb88cdf72556935fb..2de878fe2166591d3e7e1f64aabddd31b695096c 100644
--- a/gpfsl-examples/exchanger/proof_graph_piggyback.v
+++ b/gpfsl-examples/exchanger/proof_graph_piggyback.v
@@ -624,7 +624,7 @@ Lemma LTM_update γ T T' (SUB: T ⊆ T'):
   LTM_master γ T ==∗ LTM_master γ T' ∗ LTM_snap γ T'.
 Proof.
   rewrite -own_op.
-  by apply own_update, auth_update_alloc, to_agreeM_local_update.
+  by apply bi.entails_wand, own_update, auth_update_alloc, to_agreeM_local_update.
 Qed.
 Lemma LTM_snap_sub γ T T' (Le: T ⊆ T') : LTM_snap γ T' ⊢ LTM_snap γ T.
 Proof.
@@ -673,7 +673,7 @@ Qed.
 
 (** * Accessors *)
 Lemma ExchangerBaseInv_unfold_snap EI N γg γt γx x G T0 :
-  ExchangerBaseInv EI N γt γx γg x G -∗
+  ExchangerBaseInv EI N γt γx γg x G ⊢
   LTM_snapv γt T0 -∗
   ∃ LVs os T, ExchangerBaseInv_no_exist EI N γg x G γt γx LVs os T ∗ ⌜ T0 ⊆ T ⌝.
 Proof.
diff --git a/gpfsl-examples/graph/ghost.v b/gpfsl-examples/graph/ghost.v
index 1549da26a22cfc5b6b693b663b5ef00ffa2e393f..03f844fada03248805f85e1fb34dded5e7d0796c 100644
--- a/gpfsl-examples/graph/ghost.v
+++ b/gpfsl-examples/graph/ghost.v
@@ -73,7 +73,7 @@ Definition graph_snap γg G M : vProp :=
 Lemma ghost_graph_update γ G G' (Le: G ⊑ G') :
   graph_gmaster γ 1 G ==∗ graph_gmaster γ 1 G'.
 Proof.
-  apply own_update, prod_update; simpl.
+  apply bi.entails_wand, own_update, prod_update; simpl.
   - by apply mono_list_update, Le.
   - apply lat_auth_update. split; apply Le.
 Qed.
@@ -81,7 +81,7 @@ Qed.
 Lemma ghost_graph_master_snap γ q G :
   graph_gmaster γ q G -∗ graph_gsnap γ G.
 Proof.
-  apply own_mono, prod_included. split.
+  apply bi.entails_wand, own_mono, prod_included. split.
   - apply mono_list_included.
   - apply lat_auth_included.
 Qed.
@@ -90,7 +90,7 @@ Lemma ghost_graph_snap_sub γ G G' :
   G ⊑ G' →
   graph_gsnap γ G' -∗ graph_gsnap γ G.
 Proof.
-  intros Le. apply own_mono, prod_included. split.
+  intros Le. apply bi.entails_wand, own_mono, prod_included. split.
   - apply mono_list_lb_mono, Le.
   - apply lat_lb_mono. split; apply Le.
 Qed.
@@ -203,7 +203,7 @@ Proof.
 Qed.
 
 Lemma graph_master_snap_included' γg q G G' M V V' :
-  @{V} graph_master γg q G -∗ @{V'} graph_snap γg G' M -∗
+  @{V} graph_master γg q G ⊢ @{V'} graph_snap γg G' M -∗
   ⌜ G' ⊑ G ⌝.
 Proof.
   iIntros "[G _] [Gs _]". rewrite !view_at_objective_iff.
@@ -211,10 +211,10 @@ Proof.
 Qed.
 
 Lemma graph_master_snap_included γg q G G' M :
-  graph_master γg q G -∗ graph_snap γg G' M -∗ ⌜ G' ⊑ G ⌝.
+  graph_master γg q G ⊢ graph_snap γg G' M -∗ ⌜ G' ⊑ G ⌝.
 Proof. by apply view_at_wand_lr, graph_master_snap_included'. Qed.
 Lemma graph_master_snap_included_2 γg q G G' M V' :
-  graph_master γg q G -∗ @{V'} graph_snap γg G' M -∗ ⌜ G' ⊑ G ⌝.
+  graph_master γg q G ⊢ @{V'} graph_snap γg G' M -∗ ⌜ G' ⊑ G ⌝.
 Proof. by apply view_at_wand_l, graph_master_snap_included'. Qed.
 
 Lemma graph_snap_mono γg G M G' M' :
diff --git a/gpfsl-examples/history/ghost.v b/gpfsl-examples/history/ghost.v
index a22d686627f70133968b13aac35ab5282a8eb13f..8b5806b978677e61ac1b4c66c28decc0cf4d5eb4 100644
--- a/gpfsl-examples/history/ghost.v
+++ b/gpfsl-examples/history/ghost.v
@@ -60,7 +60,7 @@ Definition history_snap γg E M : vProp :=
 (* Updates *)
 Lemma ghost_history_update γ E E' (Le: E ⊑ E') :
   history_gmaster γ 1 E ==∗ history_gmaster γ 1 E'.
-Proof. by apply own_update, mono_list_update. Qed.
+Proof. by apply bi.entails_wand, own_update, mono_list_update. Qed.
 
 Lemma ghost_history_master_snap γ f E :
   history_gmaster γ f E ⊢ history_gsnap γ E.
@@ -68,7 +68,7 @@ Proof. apply own_mono, mono_list_included. Qed.
 
 Lemma ghost_history_snap_sub γ E G' :
   E ⊑ G' →
-  history_gsnap γ G' -∗ history_gsnap γ E.
+  history_gsnap γ G' ⊢ history_gsnap γ E.
 Proof. intros Le. apply own_mono, mono_list_lb_mono, Le. Qed.
 
 (* Alloc *)
@@ -144,7 +144,7 @@ Proof.
 Qed.
 
 Lemma history_master_snap_included' γg f E E' M V V' :
-  @{V} history_master γg f E -∗ @{V'} history_snap γg E' M -∗
+  @{V} history_master γg f E ⊢ @{V'} history_snap γg E' M -∗
   ⌜ E' ⊑ E ⌝.
 Proof.
   iIntros "[E _] [Es _]". rewrite !view_at_objective_iff.
@@ -152,10 +152,10 @@ Proof.
 Qed.
 
 Lemma history_master_snap_included γg q E E' M :
-  history_master γg q E -∗ history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
+  history_master γg q E ⊢ history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
 Proof. by apply view_at_wand_lr, history_master_snap_included'. Qed.
 Lemma history_master_snap_included_2 γg q E E' M V' :
-  history_master γg q E -∗ @{V'} history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
+  history_master γg q E ⊢ @{V'} history_snap γg E' M -∗ ⌜ E' ⊑ E ⌝.
 Proof. by apply view_at_wand_l, history_master_snap_included'. Qed.
 
 Lemma history_snap_mono γg E M E' M'
@@ -189,7 +189,7 @@ Qed.
 
 Lemma history_snap_lookup γg E M e dV :
   ge_view <$> E !! e = Some dV → e ∈ M →
-  history_snap γg E M -∗ ⊒(dV.(dv_comm)).
+  history_snap γg E M ⊢ ⊒(dV.(dv_comm)).
 Proof.
   intros Eqe Inm. constructor => V'' /=.
   iIntros "[_ %InM']". iPureIntro.
diff --git a/gpfsl-examples/queue/proof_hw_graph.v b/gpfsl-examples/queue/proof_hw_graph.v
index 124731c1026ef5a49b6a776241cb231c030d0b2e..646be286c331c5611b33f88114e4cfb70c3c3463 100644
--- a/gpfsl-examples/queue/proof_hw_graph.v
+++ b/gpfsl-examples/queue/proof_hw_graph.v
@@ -965,7 +965,7 @@ Qed.
 
 Lemma slots_master_slot_name_agree_L γ L T i γi :
   let slots : gmap _ _ := map_seq 0 L in
-  slots_master γ slots T -∗ slot_name γ i γi -∗
+  slots_master γ slots T ⊢ slot_name γ i γi -∗
   ⌜ fst <$> L !! i = Some γi ⌝.
 Proof.
   iIntros (slots) "SLM Gγ".
@@ -976,7 +976,7 @@ Qed.
 
 Lemma slots_master_get_pending {γq slots T i γ} v M :
   slots !! i = Some (γ, SlotUnused) →
-  slots_master γq slots T -∗ slot_reserve_tok γq i ==∗
+  slots_master γq slots T ⊢ slot_reserve_tok γq i ==∗
   slots_master γq (<[i:=(γ, SlotPending v M)]>slots) T ∗ slot_pending_tok γq i v M.
 Proof.
   iIntros (Eqi) "OM Tok". iCombine "OM Tok" as "Tok".
@@ -994,7 +994,7 @@ Qed.
 Lemma slots_master_get_pending_L {γq L T i γ} v M :
   L !! i = Some (γ, SlotUnused) →
   let slots := map_seq 0 L in
-  slots_master γq slots T -∗ slot_reserve_tok γq i ==∗
+  slots_master γq slots T ⊢ slot_reserve_tok γq i ==∗
   let slots' := map_seq 0 (<[i:=(γ, SlotPending v M)]>L) in
   slots_master γq slots' T ∗ slot_pending_tok γq i v M.
 Proof.
@@ -1069,7 +1069,7 @@ Qed.
 Lemma slots_master_set_enqueued {γq slots T i γ v M} e V :
   slots !! i = Some (γ, SlotPending v M) →
   T !! e = None →
-  slots_master γq slots T -∗
+  slots_master γq slots T ⊢
   slot_pending_tok γq i v M ==∗
   slots_master γq (<[i := (γ, SlotEnqueued (v,M,(V,e)))]>slots) (<[e := i]>T) ∗
   slot_enqueued γq i v M V e.
@@ -1091,7 +1091,7 @@ Lemma slots_master_set_enqueued_L {γq L T i γ v M} e V :
   L !! i = Some (γ, SlotPending v M) →
   T !! e = None →
   let slots := map_seq 0 L in
-  slots_master γq slots T -∗
+  slots_master γq slots T ⊢
   slot_pending_tok γq i v M ==∗
   let slots' := map_seq 0 (<[i:=(γ, SlotEnqueued (v,M,(V,e)))]>L) in
   slots_master γq slots' (<[e := i]>T) ∗ slot_enqueued γq i v M V e.
@@ -1166,7 +1166,7 @@ Qed.
 
 Lemma slots_master_slot_enqueued_agree_L γ L T i v M V e :
   let slots := map_seq 0 L in
-  slots_master γ slots T -∗ slot_enqueued γ i v M V e -∗
+  slots_master γ slots T ⊢ slot_enqueued γ i v M V e -∗
   ⌜ T !! e = Some i ∧
     (snd <$> L !! i = Some (SlotEnqueued (v,M,(V,e)))
     ∨ ∃ Vd,  snd <$> L !! i = Some (SlotDequeued (v,M,(V,e)) Vd)) ⌝.
@@ -1181,7 +1181,7 @@ Qed.
 
 Lemma slots_master_slot_enqueued_agree_L_get_enqInfo γ L T i v M V e :
   let slots := map_seq 0 L in
-  slots_master γ slots T -∗ slot_enqueued γ i v M V e -∗
+  slots_master γ slots T ⊢ slot_enqueued γ i v M V e -∗
   ⌜ T !! e = Some i ∧ get_enqInfo_L L i = Some (v,M,(V,e)) ⌝.
 Proof.
   iIntros (slots) "SM SE".
@@ -1224,7 +1224,7 @@ Qed.
 Lemma slots_master_set_dequeued {γq slots T i γ v M Ve e} Vd :
   slots !! i = Some (γ, SlotEnqueued (v,M,(Ve,e))) →
   T !! e = Some i →
-  slots_master γq slots T ==∗
+  slots_master γq slots T ⊢ |==>
   slots_master γq (<[i := (γ, SlotDequeued (v,M,(Ve,e)) Vd)]>slots) T ∗
   slot_dequeued γq i v M Ve e Vd.
 Proof.
@@ -1245,7 +1245,7 @@ Lemma slots_master_set_dequeued_L {γq L T i γ v M Ve e} Vd :
   L !! i = Some (γ, SlotEnqueued (v,M,(Ve,e))) →
   T !! e = Some i →
   let slots : gmap _ _ := map_seq 0 L in
-  slots_master γq slots T ==∗
+  slots_master γq slots T ⊢ |==>
   let slots' := map_seq 0 (<[i:=(γ, SlotDequeued (v,M,(Ve,e)) Vd)]>L) in
   slots_master γq slots' T ∗
   slot_dequeued γq i v M Ve e Vd.
@@ -1350,7 +1350,7 @@ Proof.
 Qed.
 
 Lemma SeenEnqueueds_union {γ bf n E T} M1 M2 :
-  SeenEnqueueds γ bf n E T M1 -∗ SeenEnqueueds γ bf n E T M2 -∗
+  SeenEnqueueds γ bf n E T M1 ⊢ SeenEnqueueds γ bf n E T M2 -∗
   SeenEnqueueds γ bf n E T (M1 ∪ M2).
 Proof.
   iIntros "[%Sub1 SE1] [%Sub2 SE2]".
@@ -1459,7 +1459,7 @@ Lemma own_slots_get_pending γq E q L T i γ v M :
   enq_map_enqueued T E →
   L !! i = Some (γ, SlotUnused) →
   let slots := (map_seq 0 L) in
-  slots_master γq slots T -∗
+  slots_master γq slots T ⊢
   own_slots γq E T q (map_seq 0 L) ==∗
   let slots' := map_seq 0 (<[i := (γ, SlotPending v M)]>L) in
   slots_master γq slots' T ∗ own_slots γq E T q slots' ∗ slot_pending_tok γq i v M.
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 58f5bbbf41b15f9871e878460046a459aa03d69c..60b452206a4a9a429b8e2dbda6cd621a40c8dd04 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -1196,7 +1196,7 @@ Proof. by iIntros "[? $]". Qed.
 Lemma LTM_update' γ T T' (SUB: T ⊆ T') :
   LTM_master γ T ==∗ LTM_master γ T'.
 Proof.
-  apply own_update, prod_update; [done|]. simpl.
+  apply bi.entails_wand, own_update, prod_update; [done|]. simpl.
   by apply auth_update, to_agreeM_local_update.
 Qed.
 Lemma LTM_update γ T T' (SUB: T ⊆ T') :
@@ -1238,7 +1238,7 @@ Qed.
 Lemma LEL_update' γ L L' (SUB: L ⊑ L') :
   LEL_master γ L ==∗ LEL_master γ L'.
 Proof.
-  apply own_update, prod_update; [|done]. apply prod_update; [|done]. simpl.
+  apply bi.entails_wand, own_update, prod_update; [|done]. apply prod_update; [|done]. simpl.
   by apply mono_list_update.
 Qed.
 Lemma LEL_update γ L L' (SUB: L ⊑ L') :
@@ -1276,7 +1276,7 @@ Qed.
 Lemma LDL_update' γ D D' (SUB: D ⊑ D') :
   LDL_master γ D ==∗ LDL_master γ D'.
 Proof.
-  apply own_update, prod_update; [|done]. apply prod_update; [done|]. simpl.
+  apply bi.entails_wand, own_update, prod_update; [|done]. apply prod_update; [done|]. simpl.
   by apply mono_list_update.
 Qed.
 Lemma LDL_update γ D D' (SUB: D ⊑ D') :
@@ -1354,7 +1354,7 @@ Qed.
 
 Lemma QueueInv_no_exist_QueueLocs_access γg q Q G γ γh γl η s D L T :
   let E := G.(Es) in
-  QueueInv_no_exist γg q Q G γ γh γl η s D L T -∗
+  QueueInv_no_exist γg q Q G γ γh γl η s D L T ⊢
   ∃ Vb, @{Vb} QueueLocs γg γ q E γh γl η s D L T
       ∗ (∀ Vb, @{Vb} QueueLocs γg γ q E γh γl η s D L T -∗
               QueueInv_no_exist γg q Q G γ γh γl η s D L T).
@@ -1366,7 +1366,7 @@ Qed.
 
 Lemma QueueInv_no_exist_tail_access γg q Q G γ γh γl η s D L T :
   let E := G.(Es) in
-  QueueInv_no_exist γg q Q G γ γh γl η s D L T -∗
+  QueueInv_no_exist γg q Q G γ γh γl η s D L T ⊢
   (∃ Vb (ζl : absHist),
     @{Vb} ((q >> tail) at↦{γl} ζl ∗ Tail E T ((η,s) :: D ++ L) ζl) ∗
     (∀ Vb' ζl',
@@ -1383,7 +1383,7 @@ Qed.
 
 Lemma QueueInv_no_exist_tail_immut_access γg q Q G γ γh γl η s D L T :
   let E := G.(Es) in
-  QueueInv_no_exist γg q Q G γ γh γl η s D L T -∗
+  QueueInv_no_exist γg q Q G γ γh γl η s D L T ⊢
   ∃ Vb (ζl : absHist),
     @{Vb} ((q >> tail) at↦{γl} ζl ∗ Tail E T ((η,s) :: D ++ L) ζl) ∗
     (∀ Vb', @{Vb'} (q >> tail) at↦{γl} ζl -∗
@@ -1397,7 +1397,7 @@ Qed.
 
 Lemma QueueInv_no_exist_head_immut_access γg q Q G γ γh γl η s D L T :
   let DL := (η, s) :: D in let E := G.(Es) in
-  QueueInv_no_exist γg q Q G γ γh γl η s D L T -∗
+  QueueInv_no_exist γg q Q G γ γh γl η s D L T ⊢
   (∃ Vb t0 Vs,
     @{Vb} ((q >> head) at↦{γh} toHeadHist t0 DL Vs ∗ Head γg γ E T DL Vs) ∗
     (∀ Vb', @{Vb'} ((q >> head) at↦{γh} toHeadHist t0 DL Vs) -∗
diff --git a/gpfsl-examples/queue/spec_spsc.v b/gpfsl-examples/queue/spec_spsc.v
index aa490e0d7d712ade2d1a3d944a49b3c4edff0019..4c1370ac6ea2b8448e93dc58aef292309b161f8f 100644
--- a/gpfsl-examples/queue/spec_spsc.v
+++ b/gpfsl-examples/queue/spec_spsc.v
@@ -103,7 +103,7 @@ Definition dequeue_spsc_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR qevent)}
   (dequeue : val) (Consumer : ConsumerT Σ) (SPSCInv : SPSCInvT Σ) : Prop :=
   ∀ N (DISJ: N ## histN) (q : loc) tid γg γed
     G1 M ds1 V (i := length ds1),
-  ⊒V -∗ Consumer N γg γed q G1 M ds1 -∗
+  ⊒V ⊢ Consumer N γg γed q G1 M ds1 -∗
   <<< ∀ G es ds, ▷ SPSCInv γg γed q G es ds >>>
     dequeue [ #q] @ tid; ↑N
   <<< ∃ (v: Z) V' G' ds' enqId deqId enq deq Vdeq M',
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 2a1d7fcbc6a3e944e2f03cef50023c2aa0f1a792..dc940919d3976d143db37ae44e8defdc14f3c767 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -614,13 +614,13 @@ Qed.
 Proof. constructor; [done|apply _]. Qed.
 
 Lemma ge_list_auth_lb_get γ q T :
-  ge_list_auth γ q T -∗ ge_list_lb γ T.
+  ge_list_auth γ q T ⊢ ge_list_lb γ T.
 Proof. intros. by apply embed_mono, own_mono, mono_list_included. Qed.
 Lemma ge_list_lb_mono γ T T' :
-  T' ⊑ T → ge_list_lb γ T -∗ ge_list_lb γ T'.
+  T' ⊑ T → ge_list_lb γ T ⊢ ge_list_lb γ T'.
 Proof. intros. by apply embed_mono, own_mono, mono_list_lb_mono. Qed.
 Lemma ge_list_auth_lb_get_mono γ q T T' :
-  T' ⊑ T → ge_list_auth γ q T -∗ ge_list_lb γ T'.
+  T' ⊑ T → ge_list_auth γ q T ⊢ ge_list_lb γ T'.
 Proof. intros. etrans; [apply ge_list_auth_lb_get|by apply ge_list_lb_mono]. Qed.
 
 Lemma ge_list_auth_lb_valid γ q T T' :
@@ -649,7 +649,7 @@ Qed.
 Lemma ge_list_auth_update γ T T' :
   T ⊑ T' → ge_list_auth γ 1 T ==∗ ge_list_auth γ 1 T'.
 Proof.
-  intros. rewrite -embed_bupd. by apply embed_mono, own_update, mono_list_update.
+  intros. rewrite -embed_bupd. by apply bi.entails_wand, embed_mono, own_update, mono_list_update.
 Qed.
 Lemma ge_list_auth_update' γ T T' :
   T ⊑ T' → ge_list_auth γ 1 T ==∗ ge_list_auth γ 1 T' ∗ ge_list_lb γ T'.
@@ -1440,7 +1440,7 @@ Proof.
           * iApply (view_at_mono' with "SL"); [done|].
             iClear "#". rewrite -(view_at_objective_iff (StackInv _ _ _ _ _)).
             iApply (view_at_mono with "BI"); [reflexivity|].
-            apply StackLocalLite_upgrade.
+            iApply StackLocalLite_upgrade.
           * iPureIntro. by apply (ElimStackLocalEvents_mono EL).
       - iFrame "SL'". iExists Mb'. simpl. iSplit; [|by iPureIntro].
         iApply (view_at_mono with "SLb'"); [done|]. apply StackLocalLite_from. }
@@ -2124,7 +2124,7 @@ Proof.
           * iApply (view_at_mono' with "SL"); [done|].
             iClear "#". rewrite -(view_at_objective_iff (StackInv _ _ _ _ _)).
             iApply (view_at_mono with "BI"); [reflexivity|].
-            apply StackLocalLite_upgrade.
+            iApply StackLocalLite_upgrade.
           * iPureIntro. by apply (ElimStackLocalEvents_mono EL).
       - iFrame "SL'". iExists Mb'. rewrite (StackLocalLite_from _ _ _ _ Gb').
         iFrame "SLb'". simpl. by iPureIntro. }
@@ -2373,7 +2373,7 @@ Proof.
           * iApply (view_at_mono' with "SL"); [done|].
             iClear "#". rewrite -(view_at_objective_iff (StackInv _ _ _ _ _)).
             iApply (view_at_mono with "BI"); [reflexivity|].
-            apply StackLocalLite_upgrade.
+            iApply StackLocalLite_upgrade.
           * iPureIntro. by apply (ElimStackLocalEvents_mono EL).
       - iFrame "SL'". iExists Mb'. rewrite (StackLocalLite_from _ _ _ _ Gb').
         iFrame "SLb'". simpl. by iPureIntro. }
diff --git a/gpfsl-examples/stack/proof_treiber_at.v b/gpfsl-examples/stack/proof_treiber_at.v
index 77ef622cfca4eed5e681331823d898f87d2122dd..d89e38f23a45716f2ab47fd3cdf7f18c13a4c83e 100644
--- a/gpfsl-examples/stack/proof_treiber_at.v
+++ b/gpfsl-examples/stack/proof_treiber_at.v
@@ -141,7 +141,7 @@ Global Instance TStack_persistent s : Persistent (TStack s) := _.
 
 Lemma all_slocs_node_next_access LVs n Vn :
   (Some n, Vn) ∈ LVs →
-  all_slocs LVs -∗ all_slocs LVs ∗ ∃ q on, @{Vn} n ↦{q} #(oloc_to_lit on).
+  all_slocs LVs ⊢ all_slocs LVs ∗ ∃ q on, @{Vn} n ↦{q} #(oloc_to_lit on).
 Proof.
   iIntros ([i Inn]%elem_of_list_lookup) "As".
   rewrite {1}/all_slocs (big_sepL_lookup_acc _ _ _ _ Inn).
@@ -187,7 +187,7 @@ Proof.
 Qed.
 
 Lemma in_slocs_optional_head_access S :
-  in_slocs S -∗
+  in_slocs S ⊢
     in_slocs S
     ∗ if (hd_error S) is Some n
       then ∃ on q, ⌜ next_nodes S !! 0%nat = Some on ⌝ ∧
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index 4e30ebd839b75883aaf4b3134a5995e62ddf3741..f0072a2392e2960028e1bb0cd4aac90862e3a558 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -420,7 +420,7 @@ Global Instance LTM_auth_frac_is_op q q1 q2 T :
 Proof. rewrite /LTM_auth /IsOp' /IsOp => ->. by rewrite -LTM_auth_frac_op. Qed.
 
 Lemma LTM_master_fork γ q T :
-  LTM_master γ q T -∗ LTM_snap γ T.
+  LTM_master γ q T ⊢ LTM_snap γ T.
 Proof. by apply own_mono, auth_frag_included. Qed.
 
 Lemma LTM_snap_sub γ T T' (Le: T ⊆ T') : LTM_snap γ T' ⊢ LTM_snap γ T.
@@ -456,7 +456,7 @@ Qed.
 (** Updates *)
 Lemma LTM_update' γ T T' (SUB: T ⊆ T'):
   LTM_master γ 1 T ==∗ LTM_master γ 1 T'.
-Proof. by apply own_update, auth_update, to_agreeM_local_update. Qed.
+Proof. by apply bi.entails_wand, own_update, auth_update, to_agreeM_local_update. Qed.
 Lemma LTM_update γ T T' (SUB: T ⊆ T'):
   LTM_master γ 1 T ==∗ LTM_master γ 1 T' ∗ LTM_snap γ T'.
 Proof.
@@ -606,7 +606,7 @@ Proof.
 Qed.
 
 Lemma StackLocs_no_exist_head_immut_access s E γh T S t0 LVs Vh :
-  StackLocs_no_exist s E γh T S t0 LVs Vh -∗
+  StackLocs_no_exist s E γh T S t0 LVs Vh ⊢
     let vh := (hd_error S) in
     let LVs' := (LVs ++ [(vh,Vh)]) in
     let ζh := toHeadHist t0 LVs' in
@@ -620,7 +620,7 @@ Qed.
 
 Lemma all_slocs_node_next_access LVs n Vn :
   (Some n, Vn) ∈ LVs →
-  all_slocs LVs -∗ all_slocs LVs ∗ ∃ q on, @{Vn} (n >> 0) ↦{q} #(oloc_to_lit on).
+  all_slocs LVs ⊢ all_slocs LVs ∗ ∃ q on, @{Vn} (n >> 0) ↦{q} #(oloc_to_lit on).
 Proof.
   iIntros ([i Inn]%elem_of_list_lookup) "As".
   rewrite {1}/all_slocs (big_sepL_lookup_acc _ _ _ _ Inn).
@@ -666,7 +666,7 @@ Proof.
 Qed.
 
 Lemma in_slocs_optional_head_access E T S :
-  in_slocs E T S -∗
+  in_slocs E T S ⊢
     in_slocs E T S
     ∗ if (hd_error S) is Some n
       then ∃ on q, ⌜ next_nodes S !! 0%nat = Some on ⌝ ∧ (n >> next) ↦{q} #(oloc_to_lit on)
@@ -680,7 +680,7 @@ Qed.
 Lemma StackLocs_no_exist_node_next_access s E γh T S t0 LVs Vh n Vn:
   let vh := (hd_error S) in
   (Some n, Vn) ∈ (LVs ++ [(vh,Vh)]) →
-  StackLocs_no_exist s E γh T S t0 LVs Vh -∗
+  StackLocs_no_exist s E γh T S t0 LVs Vh ⊢
     StackLocs_no_exist s E γh T S t0 LVs Vh
     ∗ ∃ q on, @{Vn} (n >> 0) ↦{q} #(oloc_to_lit on).
 Proof.
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index a1de86b7f1fb99e678cf19313c776178c1f29f2a..850f5c22fde51109e345a6112590a27dfab18045 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -972,7 +972,7 @@ Proof.
 Qed.
 
 Lemma emo_lb_own_get γ esi emo :
-  own γ (emo_auth esi emo) -∗ own γ (emo_lb esi emo).
+  own γ (emo_auth esi emo) ⊢ own γ (emo_lb esi emo).
 Proof.
   intros. apply own_mono. rewrite !prod_included. simpl. split_and!.
   - apply mono_list_included.
@@ -1349,7 +1349,7 @@ Qed.
 
 Lemma AllLinks_node_next_access mo n Vn :
   (Some n, Vn) ∈ mo →
-  AllLinks mo -∗ AllLinks mo ∗ ∃ q on, @{Vn} (n >> 0) ↦{q} #(oloc_to_lit on).
+  AllLinks mo ⊢ AllLinks mo ∗ ∃ q on, @{Vn} (n >> 0) ↦{q} #(oloc_to_lit on).
 Proof.
   iIntros ([i Inn]%elem_of_list_lookup) "AllLinks".
   rewrite {1}/AllLinks (big_sepL_lookup_acc _ _ _ _ Inn) /=.
@@ -2384,7 +2384,7 @@ Proof.
     specialize (hwf_logview_event _ EWF2 _ _ EVps). set_solver-. }
 
   (* Leak the new head node (if any) *)
-  rewrite (_ : ∀ on vs, StackNodes on vs -∗ StackNodes on vs ∗
+  rewrite (_ : ∀ on vs, StackNodes on vs ⊢ StackNodes on vs ∗
     if on is Some n
     then ∃ q onn, (n >> next) ↦{q} #(oloc_to_lit onn)
     else emp); last first.
diff --git a/gpfsl/algebra/lat_auth.v b/gpfsl/algebra/lat_auth.v
index a8ff17848f3eddb71d2edcc07d97c125fa7aa268..2008a5dc29661d6f1e102edecfa848feed2684ac 100644
--- a/gpfsl/algebra/lat_auth.v
+++ b/gpfsl/algebra/lat_auth.v
@@ -126,11 +126,11 @@ Qed.
 
 Lemma own_master_update γ a b (Ext : a ⊑ b) :
   own γ (●L a) ==∗ own γ (●L b).
-Proof. by apply own_update, lat_auth_update. Qed.
+Proof. by apply bi.entails_wand, own_update, lat_auth_update. Qed.
 
 Lemma own_master_update_join γ a b :
   own γ (●L a) ==∗ own γ (●L (a ⊔ b)).
-Proof. apply own_update, lat_auth_update_join. Qed.
+Proof. apply bi.entails_wand, own_update, lat_auth_update_join. Qed.
 
 Lemma own_snapshot_downclosed γ a b (Le : a ⊑ b) :
   own γ (◯L b) ⊢ own γ (◯L a).
diff --git a/gpfsl/algebra/lattice_cmra.v b/gpfsl/algebra/lattice_cmra.v
index 4f06edd69663b646298bc096df6b4e403049bcdc..2d9e4aa75bac7d27c05d480b062b2588bffbe3c9 100644
--- a/gpfsl/algebra/lattice_cmra.v
+++ b/gpfsl/algebra/lattice_cmra.v
@@ -123,7 +123,7 @@ Section lat_auth.
     own γ (● (to_latT V)) ==∗ own γ (● (to_latT V')) ∗ own γ (◯ (to_latT V')).
   Proof.
     rewrite -own_op.
-    by apply own_update, auth_update_alloc, latT_local_unit_update.
+    by apply bi.entails_wand, own_update, auth_update_alloc, latT_local_unit_update.
   Qed.
 
   Lemma own_lat_auth_update_fork γ (V: LAT):
diff --git a/gpfsl/base_logic/bi.v b/gpfsl/base_logic/bi.v
index f2c84f113df437e93f9fcd77e77bac90fef07929..fda8cdb40e6cdaa099ee8ef4d0f1632af329c381 100644
--- a/gpfsl/base_logic/bi.v
+++ b/gpfsl/base_logic/bi.v
@@ -44,7 +44,7 @@ Proof. intros ??. eauto. Qed.
 Lemma monPred_in_intro_incl `{BiAffine PROP} P i' :
   P -∗ ⊒i' -∗ ∃ i, ⊒i ∧ ⌜i' ⊑ i⌝ ∧ ⎡ P i ⎤.
 Proof.
-  apply bi.wand_intro_r. iIntros "P".
+  apply bi.entails_wand, bi.wand_intro_r. iIntros "P".
   iDestruct (monPred_in_intro with "P") as (i) "(V & P & %)". eauto.
 Qed.
 
diff --git a/gpfsl/base_logic/frame_instances.v b/gpfsl/base_logic/frame_instances.v
index f76c42595658e431735b07bf5b3c1eb999dd5da3..0a633d2f19449f64fc6bbf76bad20a96e28e1cca 100644
--- a/gpfsl/base_logic/frame_instances.v
+++ b/gpfsl/base_logic/frame_instances.v
@@ -24,7 +24,7 @@ Proof. Fail iIntros "[$ $]". Abort.
 Proof.
   rewrite /Frame /IsBiIndexRel -view_join_intuitionistically_if => -> H.
   rewrite -view_join_sep.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 
 #[global] Instance frame_view_join_view_mono_emp p P V1 V2 :
@@ -47,7 +47,7 @@ Proof. Fail iIntros "$". Abort.
 Proof.
   rewrite /Frame => H.
   rewrite (view_join_intro_current R V) -view_join_intuitionistically_if -view_join_sep.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 Example test_after R V : R ⊢ ⊔{V} R.
 Proof. iIntros "$". Abort.
@@ -72,7 +72,7 @@ Proof. Fail iIntros "[$ $]". Abort.
 Proof.
   rewrite /Frame /IsBiIndexRel -view_at_intuitionistically_if => ->.
   rewrite view_at_to_view_join -view_join_sep => ?.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 Example test_after P Q V :
   @{V} P ∗ ⊔{V} Q ⊢ ⊔{V} (P ∗ Q).
@@ -107,7 +107,7 @@ Qed.
 Proof.
   rewrite /Frame /IsBiIndexRel -view_at_intuitionistically_if => -> H.
   rewrite -view_at_sep.
-  by apply view_at_wand_2, view_at_at, bi.entails_wand.
+  by apply bi.wand_entails, view_at_wand_2, view_at_at, bi.entails_wand.
 Qed.
 
 #[global] Instance frame_view_at_view_mono_emp p P V1 V2 :
diff --git a/gpfsl/base_logic/history.v b/gpfsl/base_logic/history.v
index 4b6e4bb3bde0b4f4cd61885d77e860467312df30..a653d8212f353ee4638ee88f027546696cb2385e 100644
--- a/gpfsl/base_logic/history.v
+++ b/gpfsl/base_logic/history.v
@@ -344,7 +344,7 @@ Section hist.
 
   Lemma hist_frac_1 l p C:
     hist l p C ⊢ ⌜ ✓ p ⌝.
-  Proof. by rewrite hist_eq /hist_def mapsto_valid. Qed.
+  Proof. rewrite hist_eq /hist_def. iApply mapsto_valid. Qed.
 
   (** Properties of freeable blocks *)
   Global Instance hist_freeable_timeless q l n : Timeless (†{q}l…n).
@@ -841,6 +841,7 @@ Section hist.
     rewrite (alloc_step_cell_list_map _ _ _ _ _ _ _ ALLOC).
     inversion_clear ALLOC. inversion_clear MEMALL. rewrite -LEN.
     inversion_clear DRFPost. clear ALLOC LEN VALL n.
+    apply bi.entails_wand.
     revert l M' Vc AMES ADD FRESH LE.
     induction 𝑚s as [|𝑚 𝑚s IH] => l M3 Vc AMES ADD FRESH LE.
     { inversion ADD; subst; simpl in *. iIntros "(o1 & o2 & o3 & o4)".
@@ -1304,7 +1305,7 @@ Section hist.
     let Vc' o 𝑚 : view
       := (if decide (Relaxed ⊑ o)
           then add_awrite_id Vc l 𝑚.(mto) else set_write_time Vc l 𝑚.(mto)) in
-    gen_heap_interp (to_hist (mem_cut M1 Vc)) -∗ hist l 1 C -∗
+    gen_heap_interp (to_hist (mem_cut M1 Vc)) ⊢ hist l 1 C -∗
     □ ∀ o 𝑚 (Vr: view) (M2: memory) 𝓥1 𝓥2 𝓝1 𝓝2,
       ⌜𝑚.(mloc) = l ∧
         write_step 𝓥1 M1 𝑚 o Vr 𝓥2 M2 ∧
diff --git a/gpfsl/base_logic/meta_data.v b/gpfsl/base_logic/meta_data.v
index e37875d022603f09fb0fb4ab7efa515191de88d5..08127ac6bedfc09c17dfcbfa084b164369d9d0fb 100644
--- a/gpfsl/base_logic/meta_data.v
+++ b/gpfsl/base_logic/meta_data.v
@@ -77,6 +77,6 @@ Section meta_vprop.
   Proof.
     intros.
     rewrite meta_token_eq meta_eq /meta_token_def /meta_def -embed_bupd.
-    by apply embed_mono, gen_heap.meta_set.
+    by apply bi.entails_wand, embed_mono, bi.wand_entails, gen_heap.meta_set.
   Qed.
 End meta_vprop.
diff --git a/gpfsl/base_logic/na.v b/gpfsl/base_logic/na.v
index 5a8a850c6813169faee2c763077d878d72dd617b..66ca5755f8a3a3d3f0a3d47d8695a9d7b5f415de 100644
--- a/gpfsl/base_logic/na.v
+++ b/gpfsl/base_logic/na.v
@@ -152,7 +152,7 @@ Section na_props.
   Qed.
 
   Lemma own_loc_prim_combine l q1 q2 C1 C2 :
-    l p↦{q1} C1 -∗ l p↦{q2} C2 -∗ l p↦{q1 + q2} C1.
+    l p↦{q1} C1 ⊢ l p↦{q2} C2 -∗ l p↦{q1 + q2} C1.
   Proof.
     iIntros "H1 H2". iDestruct (own_loc_prim_agree with "H1 H2") as %<-. iFrame.
   Qed.
@@ -220,7 +220,7 @@ Section na_props.
 
   Lemma own_loc_na_own_loc_prim l v q :
     l ↦{q} v ⊢ ∃ C, l p↦{q} C.
-  Proof. rewrite -own_loc_own_loc_prim. apply own_loc_na_own_loc. Qed.
+  Proof. rewrite -own_loc_own_loc_prim. apply bi.wand_entails, own_loc_na_own_loc. Qed.
 
   Lemma own_loc_prim_hist l q C : l p↦{q} C ⊢ ⎡ hist l q C ⎤.
   Proof. iDestruct 1 as (??? _) "(_ & _ & _ & _ & $ & _)". Qed.
diff --git a/gpfsl/base_logic/vprop.v b/gpfsl/base_logic/vprop.v
index a01b4052182dce4b92b44f526938be792e8ea994..5cf50216dc76a3d2b6a43e4192107363eee81d55 100644
--- a/gpfsl/base_logic/vprop.v
+++ b/gpfsl/base_logic/vprop.v
@@ -220,21 +220,21 @@ Proof. un_va_2. rewrite monPred_objectively_unfold embed_forall. eauto. Qed.
 
 (* Convenient lemmas to create specialized instances that drop views *)
 Lemma view_at_wand_l P Q R :
-  (∀ V1 V2, @{V1} P -∗ @{V2} Q -∗ R) → ∀ V2, P -∗ @{V2} Q -∗ R.
+  (∀ V1 V2, @{V1} P ⊢ @{V2} Q -∗ R) → ∀ V2, P ⊢ @{V2} Q -∗ R.
 Proof.
   intros IMPL V2. iIntros "P".
   iDestruct (view_at_intro with "P") as (V1) "[_ P]". iApply (IMPL with "P").
 Qed.
 
 Lemma view_at_wand_r P Q R :
-  (∀ V1 V2, @{V1} P -∗ @{V2} Q -∗ R) → ∀ V1, @{V1} P -∗ Q -∗ R.
+  (∀ V1 V2, @{V1} P ⊢ @{V2} Q -∗ R) → ∀ V1, @{V1} P ⊢ Q -∗ R.
 Proof.
   intros IMPL V1. iIntros "P Q".
   iDestruct (view_at_intro with "Q") as (V2) "[_ Q]". iApply (IMPL with "P Q").
 Qed.
 
 Lemma view_at_wand_lr P Q R :
-  (∀ V1 V2, @{V1} P -∗ @{V2} Q -∗ R) → P -∗ Q -∗ R.
+  (∀ V1 V2, @{V1} P ⊢ @{V2} Q -∗ R) → P ⊢ Q -∗ R.
 Proof.
   intros IMPL. iIntros "P Q".
   iDestruct (view_at_intro with "Q") as (V2) "[_ Q]".
@@ -341,7 +341,7 @@ Proof. by un_vj. Qed.
 Lemma view_join_except_0 P V : ⊔{V} ◇ P ⊣⊢ ◇ ⊔{V} P.
 Proof. by un_vj. Qed.
 
-Lemma view_join_mono_I P Q V : (P -∗ Q) -∗ (⊔{V} P -∗ ⊔{V} Q).
+Lemma view_join_mono_I P Q V : (P -∗ Q) ⊢ (⊔{V} P -∗ ⊔{V} Q).
 Proof. intros_vj. iIntros "PQ" (? ->). rewrite /= -monPred_wand_force. eauto. Qed.
 
 #[global] Instance view_join_ne V : NonExpansive (view_join V : _ → vProp).
@@ -369,18 +369,18 @@ Proof. intros ??. rewrite view_join_eq /=. by apply objective_at. Qed.
 #[global] Instance view_join_timeless P V : Timeless P → Timeless (⊔{V} P).
 Proof.
   intros. rewrite /Timeless -view_join_later -view_join_except_0.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 
 #[global] Instance view_join_persistent P V : Persistent P → Persistent (⊔{V} P).
 Proof.
   intros. rewrite /Persistent -view_join_persistently.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 #[global] Instance view_join_absorbing P V : Absorbing P → Absorbing (⊔{V} P).
 Proof.
   intros. rewrite /Absorbing -view_join_absorbingly.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 #[global] Instance view_join_affine P V : Affine P → Affine (⊔{V} P).
 Proof. intros [AF]. rewrite /Affine. intros_vj. rewrite AF. eauto. Qed.
@@ -403,7 +403,7 @@ Proof.
   - iIntros "P". iApply "P"; iPureIntro; solve_lat.
 Qed.
 
-Lemma view_join_intro_current P V : P -∗ ⊔{V} P.
+Lemma view_join_intro_current P V : P ⊢ ⊔{V} P.
 Proof. rewrite view_join_unfold. eauto. Qed.
 
 Lemma view_join_intro_at P V1 V2 : @{V1 ⊔ V2} P -∗ ⊒V1 -∗ ⊔{V2} P.
@@ -456,7 +456,7 @@ Proof. rewrite -!view_join_unfold. by apply view_join_join_l. Qed.
 Lemma monPred_in_join P Q V : (⊒V → P) ∗ Q ⊢ ⊒V → P ∗ Q.
 Proof. rewrite -!view_join_unfold. by apply view_join_join_r. Qed.
 
-Lemma monPred_in_view_elim P V : (⊒V → P) -∗ ⎡ ∃ V', P V' ⎤.
+Lemma monPred_in_view_elim P V : (⊒V → P) ⊢ ⎡ ∃ V', P V' ⎤.
 Proof.
   constructor=> Vx. iIntros "H". iExists (V ⊔ Vx). iApply "H". iPureIntro. solve_lat.
 Qed.
@@ -514,7 +514,7 @@ Proof. rewrite /FromPure=> <-. by rewrite -{1}view_join_pure view_join_affinely_
   IntoWand p q R P Q → IntoWand p q (⊔{V} R) (⊔{V} P) (⊔{V} Q).
 Proof.
   rewrite /IntoWand -!view_join_intuitionistically_if -view_join_wand => ?.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 #[global] Instance from_wand_view_join P Q1 Q2 V :
   FromWand P Q1 Q2 → FromWand (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2).
@@ -529,7 +529,7 @@ Proof. by rewrite /FromImpl -view_join_impl => <-. Qed.
 Proof.
   rewrite /IntoAnd -view_join_and=> HP.
   rewrite -!view_join_intuitionistically_if.
-  by apply view_join_wand_2, view_join_at, bi.entails_wand.
+  by apply bi.wand_entails, view_join_wand_2, view_join_at, bi.entails_wand.
 Qed.
 #[global] Instance from_and_view_join P Q1 Q2 V :
   FromAnd P Q1 Q2 → FromAnd (⊔{V} P) (⊔{V} Q1) (⊔{V} Q2).
@@ -650,7 +650,7 @@ Proof. by rewrite /IntoEmbed view_at_eq. Qed.
   IntoWand p q R P Q → IntoWand p q (@{V} R) (@{V} P) (@{V} Q).
 Proof.
   rewrite /IntoWand -!view_at_intuitionistically_if -view_at_wand => ?.
-  by apply view_at_wand_2, view_at_at, bi.entails_wand.
+  by apply bi.wand_entails, view_at_wand_2, view_at_at, bi.entails_wand.
 Qed.
 (* no FromWand and FromImpl instance for view_at: they don't hold. *)
 
@@ -659,7 +659,7 @@ Qed.
 Proof.
   rewrite /IntoAnd -view_at_and=> HP.
   rewrite -!view_at_intuitionistically_if.
-  by apply view_at_wand_2, view_at_at, bi.entails_wand.
+  by apply bi.wand_entails, view_at_wand_2, view_at_at, bi.entails_wand.
 Qed.
 #[global] Instance from_and_view_at P Q1 Q2 V :
   FromAnd P Q1 Q2 → FromAnd (@{V} P) (@{V} Q1) (@{V} Q2).
diff --git a/gpfsl/gps/middleware_PP.v b/gpfsl/gps/middleware_PP.v
index 82dccfc0a7b532fc1f9695ad9cbe6e7a8b285bae..f484e825741f77b89a8476ab0287be0d534404ee 100644
--- a/gpfsl/gps/middleware_PP.v
+++ b/gpfsl/gps/middleware_PP.v
@@ -38,7 +38,7 @@ Section PP.
   Qed.
 
   Lemma GPS_PPInv_own_loc_prim b γ :
-    ▷?b GPS_PPInv γ -∗ ∃ C, ▷?b own_loc_prim l 1 C.
+    ▷?b GPS_PPInv γ ⊢ ∃ C, ▷?b own_loc_prim l 1 C.
   Proof.
     rewrite GPS_PPInv_eq /GPS_PPInv_def gps_inv_own_loc_prim.
     iDestruct 1 as (C) "?". iExists C. iNext. by iFrame.
diff --git a/gpfsl/gps/middleware_SW.v b/gpfsl/gps/middleware_SW.v
index a2d5572e3e252e0cc2f1addac47e72a62a4aa1f5..2ee1efa904d1ccf84cefe3c04e8fd0eaff519c9a 100644
--- a/gpfsl/gps/middleware_SW.v
+++ b/gpfsl/gps/middleware_SW.v
@@ -117,7 +117,7 @@ Proof. apply: frame_fractional. Qed.
   (* Unfolding *)
   #[local] Lemma GPS_SWWriter_from_SW γs γl ζ t s v V :
     ζ !! t = Some (v, V) → no_earlier_time ζ t →
-    gps_snap γs {[t := s]} -∗ l sw⊒{γl} ζ -∗
+    gps_snap γs {[t := s]} ⊢ l sw⊒{γl} ζ -∗
     GPS_SWWriter t s v (encode (γs, γl)).
   Proof.
     rewrite GPS_SWWriter_eq. iIntros (EQ ?) "S W". iExists _, γs, γl.
@@ -126,7 +126,7 @@ Proof. apply: frame_fractional. Qed.
   Qed.
 
   #[local] Lemma GPS_SWWriter_from_SW_singleton γs γl t s v V :
-    gps_snap γs {[t := s]} -∗ l sw⊒{γl} {[t := (v, V)]} -∗
+    gps_snap γs {[t := s]} ⊢ l sw⊒{γl} {[t := (v, V)]} -∗
     GPS_SWWriter t s v (encode (γs, γl)).
   Proof.
     apply : GPS_SWWriter_from_SW.
@@ -223,7 +223,7 @@ Proof. apply: frame_fractional. Qed.
   Qed.
 
   Lemma GPS_SWSharedWriter_Reader t s v γ :
-    GPS_SWSharedWriter t s v γ -∗ GPS_Reader l t s v γ.
+    GPS_SWSharedWriter t s v γ ⊢ GPS_Reader l t s v γ.
   Proof.
     rewrite GPS_SWSharedWriter_eq GPS_Reader_eq.
     iDestruct 1 as (ζ γs γl ENC) "(Gs & SY & W & %IS & %MAX)".
@@ -233,7 +233,7 @@ Proof. apply: frame_fractional. Qed.
   Qed.
 
   Lemma GPS_SWSharedReader_Reader t s v q γ:
-    GPS_SWSharedReader t s v q γ -∗ GPS_Reader l t s v γ.
+    GPS_SWSharedReader t s v q γ ⊢ GPS_Reader l t s v γ.
   Proof. rewrite GPS_SWSharedReader_eq. by iIntros "[$ ?]". Qed.
 
   Lemma GPS_SWSharedReader_Reader_join_subjectively t s v s' v' q γ:
@@ -309,7 +309,7 @@ Proof. apply: frame_fractional. Qed.
   Qed.
 
   Lemma GPS_SWSharedWriter_latest_time_view t t' s s' v v' γ V1 V2 :
-    @{V1} GPS_SWSharedWriter t s v γ -∗ @{V2} GPS_Reader l t' s' v' γ -∗ ⌜t' ⊑ t⌝.
+    @{V1} GPS_SWSharedWriter t s v γ ⊢ @{V2} GPS_Reader l t' s' v' γ -∗ ⌜t' ⊑ t⌝.
   Proof.
     rewrite GPS_Reader_eq. iIntros "SR". iDestruct 1 as (γs γl V ENC) "[_ SN]".
     rewrite (GPS_SWSharedWriter_unfold ENC).
@@ -320,10 +320,10 @@ Proof. apply: frame_fractional. Qed.
     iPureIntro. apply MAX. by eexists.
   Qed.
   Lemma GPS_SWSharedWriter_latest_time_2 t t' s s' v v' γ V2 :
-    GPS_SWSharedWriter t s v γ -∗ @{V2} GPS_Reader l t' s' v' γ -∗ ⌜t' ⊑ t⌝.
+    GPS_SWSharedWriter t s v γ ⊢ @{V2} GPS_Reader l t' s' v' γ -∗ ⌜t' ⊑ t⌝.
   Proof. by apply view_at_wand_l, GPS_SWSharedWriter_latest_time_view. Qed.
   Lemma GPS_SWSharedWriter_latest_time_1 t t' s s' v v' γ:
-    GPS_SWSharedWriter t s v γ -∗ GPS_Reader l t' s' v' γ -∗ ⌜t' ⊑ t⌝.
+    GPS_SWSharedWriter t s v γ ⊢ GPS_Reader l t' s' v' γ -∗ ⌜t' ⊑ t⌝.
   Proof. by apply view_at_wand_lr, GPS_SWSharedWriter_latest_time_view. Qed.
 
   Lemma GPS_SWSharedWriter_latest_time t t' s s' v v' q γ:
diff --git a/gpfsl/gps/model_defs.v b/gpfsl/gps/model_defs.v
index d95c43668fdfcf5c9c7aaa36fce69aa7bb7ef43d..005632cad3212e4034349895a890ba1523d6bc47 100644
--- a/gpfsl/gps/model_defs.v
+++ b/gpfsl/gps/model_defs.v
@@ -272,7 +272,7 @@ Section Properties.
     gps_own γ χ ==∗ gps_own γ (<[t := s]> χ).
   Proof.
     rewrite -embed_bupd.
-    by apply embed_mono, own_update, auth_update, to_agreeM_local_update_insert.
+    by apply bi.entails_wand, embed_mono, own_update, auth_update, to_agreeM_local_update_insert.
   Qed.
   Lemma gps_own_insert γ χ t s (FRESH: χ !! t = None) :
     gps_own γ χ ==∗ gps_own γ (<[t := s]> χ) ∗ gps_snap γ ({[ t := s ]}).
@@ -333,7 +333,7 @@ Section Properties.
   Qed.
 
   Lemma gps_inv_own_loc_prim IW γ bs :
-    gps_inv IP IW l γ bs -∗ ∃ C, l p↦ C.
+    gps_inv IP IW l γ bs ⊢ ∃ C, l p↦ C.
   Proof.
     iDestruct 1 as (μ ?????) "(? & SW & ?)".
     by iApply (AtomicPtsToX_own_loc_prim with "SW").
@@ -345,13 +345,13 @@ Section Properties.
   Proof. rewrite GPS_Reader_eq. apply PrtSync_PrtSeen. Qed.
 
   Lemma GPS_Reader_from_seen_singleton γs γl t s v V :
-    gps_snap γs {[t := s]} -∗ l sn⊒{γl} {[t := (v, V)]} -∗
+    gps_snap γs {[t := s]} ⊢ l sn⊒{γl} {[t := (v, V)]} -∗
     GPS_Reader l t s v (encode (γs, γl)).
   Proof.
     rewrite GPS_Reader_eq. iIntros "S R". iExists γs, γl, _. by iFrame "S R".
   Qed.
   Lemma GPS_Reader_from_sync_singleton γs γl t s v V :
-    gps_snap γs {[t := s]} -∗ l sy⊒{γl} {[t := (v, V)]} -∗
+    gps_snap γs {[t := s]} ⊢ l sy⊒{γl} {[t := (v, V)]} -∗
     GPS_Reader l t s v (encode (γs, γl)).
   Proof.
     rewrite AtomicSync_AtomicSeen. apply GPS_Reader_from_seen_singleton.
diff --git a/gpfsl/gps/model_rules_cas.v b/gpfsl/gps/model_rules_cas.v
index f99a138ac96344454b4d55ad98ce5592b2000c67..6b254944c50c2b6de54373dc223911ed69896cf6 100644
--- a/gpfsl/gps/model_rules_cas.v
+++ b/gpfsl/gps/model_rules_cas.v
@@ -573,7 +573,7 @@ Section CAS.
       iAssert (@{Vw} GPS_Reader l t s vw γ)%I with "[SY2]" as "#PSY'".
       { iApply (view_at_mono' with "SY2"); [done|].
         iApply (view_at_mono with "[SS']"); [reflexivity|..|].
-        - rewrite ENC. apply GPS_Reader_from_sync_singleton.
+        - rewrite ENC. iApply GPS_Reader_from_sync_singleton.
         - by iFrame "Gs'". }
 
       have LeVrw : Vs V Vrel ow ⊔ Vr ⊑ Vw.
diff --git a/gpfsl/gps/model_rules_write.v b/gpfsl/gps/model_rules_write.v
index 237b4052aaf6c9286a0dc4ad0d747061bbd8ce7f..66acc3fb55f8874dc5a4b420fb099405dca1e3a5 100644
--- a/gpfsl/gps/model_rules_write.v
+++ b/gpfsl/gps/model_rules_write.v
@@ -211,7 +211,7 @@ Section Write.
     (Eqsx: sx = μ tx) :
     let ζ' : absHist := <[t':=(v',V')]> ζ in
     let μ' := <[t':=s']> μ in
-    resBE IP IW l γ μ ζ tx -∗
+    resBE IP IW l γ μ ζ tx ⊢
     resD IP IW l γ μ ζ tx -∗
     @{Vx} F γ tx sx vx ∗
     (@{V'} F γ t' s' v' -∗
diff --git a/gpfsl/logic/atomic_ghost.v b/gpfsl/logic/atomic_ghost.v
index 3471fe49ef8021be5a9aa2b0e2499af1849d2297..6f5180fc9d09a664585a9911bccd8229012f82a2 100644
--- a/gpfsl/logic/atomic_ghost.v
+++ b/gpfsl/logic/atomic_ghost.v
@@ -54,7 +54,7 @@ Implicit Types (P Q R : vProp).
           -?Some_op -?frac_auth_frag_op -?pair_op
           ?histBase_idemp ?agree_idemp ?left_id ?right_id.
 #[local] Ltac intro_own_valid :=
-  apply bi.wand_intro_r; rewrite_own_op; rewrite own_valid.
+  apply bi.entails_wand, bi.wand_intro_r; rewrite_own_op; rewrite own_valid.
 
 Lemma at_full_auth_unfold γ ζ tx Va :
   at_auth γ ζ tx Va ⊣⊢
@@ -110,7 +110,7 @@ Lemma at_exclusive_write_update γ t t':
   at_auth_exclusive_write γ t -∗ at_exclusive_write γ t 1%Qp
   ==∗ at_auth_exclusive_write γ t' ∗ at_exclusive_write γ t' 1%Qp.
 Proof.
-  apply bi.wand_intro_r. rewrite_own_op.
+  apply bi.entails_wand, bi.wand_intro_r. rewrite_own_op.
   apply own_update. apply prod_update; [done|]. apply prod_update; [|done].
   by apply frac_auth_update_1.
 Qed.
@@ -174,14 +174,14 @@ Proof. iIntros "(AW & EX & NA)". by iApply at_auth_writer_exact. Qed.
 Lemma at_writer_base_update γ ζ ζ' (Sub: ζ ⊆ ζ'):
   at_writer_base γ ζ 1 ==∗ at_writer_base γ ζ' 1.
 Proof.
-  apply own_update, prod_update; simpl; [|done].
+  apply bi.entails_wand, own_update, prod_update; simpl; [|done].
   by apply auth_update, toHistBase_local_update.
 Qed.
 Lemma at_writer_update γ ζ ζ' (Sub: ζ ⊆ ζ'):
   at_auth_writer γ ζ -∗ at_writer γ ζ ==∗ at_auth_writer γ ζ' ∗ at_writer γ ζ'.
 Proof.
-  apply bi.wand_intro_r. rewrite -!fractional Qp.quarter_three_quarter.
-  by apply at_writer_base_update.
+  apply bi.entails_wand, bi.wand_intro_r. rewrite -!fractional Qp.quarter_three_quarter.
+  by apply bi.wand_entails, at_writer_base_update.
 Qed.
 Lemma at_writer_update' γ ζ0 ζ ζ' (Sub: ζ ⊆ ζ'):
   at_auth_writer γ ζ0 -∗ at_writer γ ζ ==∗ at_auth_writer γ ζ' ∗ at_writer γ ζ'.
@@ -215,7 +215,7 @@ Proof. iIntros "[? _]". by iApply at_auth_writer_latest. Qed.
 Lemma at_reader_extract γ ζ1 ζ2 (Sub: ζ2 ⊆ ζ1) :
   at_reader γ ζ1 -∗ at_reader γ ζ2.
 Proof.
-  apply own_mono, prod_included. split; [|done].
+  apply bi.entails_wand, own_mono, prod_included. split; [|done].
   by apply auth_frag_mono, toHistBase_included.
 Qed.
 
@@ -237,14 +237,14 @@ Proof.
 Qed.
 
 Lemma at_writer_base_fork_at_reader γ q ζ :
-  at_writer_base γ ζ q -∗ at_reader γ ζ.
+  at_writer_base γ ζ q ⊢ at_reader γ ζ.
 Proof. by iIntros "[_ $]". Qed.
 Lemma at_writer_base_fork_at_reader_sub γ q ζ ζ' (Sub: ζ' ⊆ ζ):
-  at_writer_base γ ζ q -∗ at_reader γ ζ'.
-Proof. rewrite at_writer_base_fork_at_reader. by apply at_reader_extract. Qed.
+  at_writer_base γ ζ q ⊢ at_reader γ ζ'.
+Proof. rewrite at_writer_base_fork_at_reader. by apply bi.wand_entails, at_reader_extract. Qed.
 Lemma at_writer_base_fork_at_reader_singleton γ q ζ t vV
   (HL: ζ !! t = Some vV):
-  at_writer_base γ ζ q -∗ at_reader γ {[t:= vV]}.
+  at_writer_base γ ζ q ⊢ at_reader γ {[t:= vV]}.
 Proof. by apply at_writer_base_fork_at_reader_sub, map_singleton_subseteq_l. Qed.
 Lemma at_writer_base_at_reader_singleton_sub γ q ζ t vV:
   at_writer_base γ ζ q -∗ at_reader γ {[t := vV]} -∗ ⌜ζ !! t = Some vV⌝.
@@ -254,27 +254,27 @@ Proof.
   by case lookup eqn:Eq => [/=->|//].
 Qed.
 
-Lemma at_writer_fork_at_reader γ ζ : at_writer γ ζ -∗ at_reader γ ζ.
+Lemma at_writer_fork_at_reader γ ζ : at_writer γ ζ ⊢ at_reader γ ζ.
 Proof. by apply at_writer_base_fork_at_reader. Qed.
 Lemma at_writer_fork_at_reader_sub γ ζ ζ' (Sub: ζ' ⊆ ζ):
-  at_writer γ ζ -∗ at_reader γ ζ'.
+  at_writer γ ζ ⊢ at_reader γ ζ'.
 Proof. by apply at_writer_base_fork_at_reader_sub. Qed.
 Lemma at_writer_fork_at_reader_singleton γ ζ t vV (HL: ζ !! t = Some vV):
-  at_writer γ ζ -∗ at_reader γ {[t:= vV]}.
+  at_writer γ ζ ⊢ at_reader γ {[t:= vV]}.
 Proof. by apply at_writer_base_fork_at_reader_singleton. Qed.
 Lemma at_writer_at_reader_singleton_sub γ ζ t vV:
   at_writer γ ζ -∗ at_reader γ {[t := vV]} -∗ ⌜ζ !! t = Some vV⌝.
 Proof. by apply at_writer_base_at_reader_singleton_sub. Qed.
 
 Lemma at_auth_writer_fork_at_reader γ ζ :
-  at_auth_writer γ ζ -∗ at_reader γ ζ.
+  at_auth_writer γ ζ ⊢ at_reader γ ζ.
 Proof. by apply at_writer_base_fork_at_reader. Qed.
 Lemma at_auth_writer_fork_at_reader_sub γ ζ ζ' (Sub: ζ' ⊆ ζ) :
-  at_auth_writer γ ζ -∗ at_reader γ ζ'.
+  at_auth_writer γ ζ ⊢ at_reader γ ζ'.
 Proof. by apply at_writer_base_fork_at_reader_sub. Qed.
 Lemma at_auth_writer_fork_at_reader_singleton γ ζ t vV
   (HL: ζ !! t = Some vV) :
-  at_auth_writer γ ζ -∗ at_reader γ {[t:= vV]}.
+  at_auth_writer γ ζ ⊢ at_reader γ {[t:= vV]}.
 Proof. by apply at_writer_base_fork_at_reader_singleton. Qed.
 Lemma at_auth_writer_at_reader_singleton_sub γ ζ t vV :
   at_auth_writer γ ζ -∗ at_reader γ {[t := vV]} -∗ ⌜ζ !! t = Some vV⌝.
diff --git a/gpfsl/logic/atomic_ops.v b/gpfsl/logic/atomic_ops.v
index 383abfc99015566fe6a78bf06d52935888a7e68e..1915b7b54e0f93c91f24d8981a83d31e389680dc 100644
--- a/gpfsl/logic/atomic_ops.v
+++ b/gpfsl/logic/atomic_ops.v
@@ -762,7 +762,7 @@ Lemma AtomicSeen_CASX_later
   (∀ t v, no_earlier_time ζ' t → fst <$> ζ !! t = Some v →
           ∃ vl : lit, v = #vl ∧ lit_comparable vr vl) →
   let Wv ζ : vProp := (if mo is SingleWriter then ⎡ at_writer γ ζ ⎤ else True)%I in
-  l sn⊒{γ} ζ' -∗
+  l sn⊒{γ} ζ' ⊢
   @{Vb} AtomicPtsToX l γ tx ζ mo -∗
   ⊒V -∗
   (if decide (AcqRel ⊑ ow) then True else △{tid} ⊒Vrel) -∗
diff --git a/gpfsl/logic/atomic_preds.v b/gpfsl/logic/atomic_preds.v
index 7f3333f0cdf3654b9d1061d1544f1061426d409b..6d14a2fcdb8d357994463d49ec78a49ec7901bc1 100644
--- a/gpfsl/logic/atomic_preds.v
+++ b/gpfsl/logic/atomic_preds.v
@@ -397,14 +397,14 @@ Proof.
 Qed.
 
 Lemma AtomicPtsTo_exclusive_obj l γ1 ζ1 md1 γ2 ζ2 md2 V1 V2 :
-  @{V1} AtomicPtsTo l γ1 ζ1 md1 -∗ @{V2} AtomicPtsTo l γ2 ζ2 md2 -∗ False.
+  @{V1} AtomicPtsTo l γ1 ζ1 md1 ⊢ @{V2} AtomicPtsTo l γ2 ζ2 md2 -∗ False.
 Proof.
   rewrite AtomicPtsTo_eq.
   iIntros "[% H1] [% H2]". iApply (AtomicPtsToX_exclusive_obj with "H1 H2").
 Qed.
 
 Lemma AtomicPtsTo_exclusive l γ1 ζ1 md1 γ2 ζ2 md2:
-  AtomicPtsTo l γ1 ζ1 md1 -∗ AtomicPtsTo l γ2 ζ2 md2 -∗ False.
+  AtomicPtsTo l γ1 ζ1 md1 ⊢ AtomicPtsTo l γ2 ζ2 md2 -∗ False.
 Proof. apply view_at_wand_lr, AtomicPtsTo_exclusive_obj. Qed.
 
 (** SeenLocal and SyncLocal *)
@@ -467,7 +467,7 @@ Qed.
 
 Lemma SeenLocal_SyncLocal_singleton l t v V :
   let ζ := {[t := (v, V)]} in
-  ⊒V -∗ SeenLocal l ζ -∗ SyncLocal l ζ : vProp.
+  ⊒V ⊢ SeenLocal l ζ -∗ SyncLocal l ζ : vProp.
 Proof.
   iIntros (ζ) "SV SL". rewrite /SeenLocal /SyncLocal.
   iIntros (t0 V0 Eq0). rewrite seen_view_seen_time.
@@ -580,7 +580,7 @@ Proof.
 Qed.
 
 Lemma AtomicSeen_mono l γ ζ1 ζ2 (NE: ζ2 ≠ ∅) (SUB: ζ2 ⊆ ζ1) :
-  l sn⊒{γ} ζ1 -∗ l sn⊒{γ} ζ2.
+  l sn⊒{γ} ζ1 ⊢ l sn⊒{γ} ζ2.
 Proof.
   rewrite AtomicSeen_eq. iIntros "(SL & SR & Va)". iDestruct "Va" as (Va ?) "NA".
   iSplit; last iSplit.
@@ -609,7 +609,7 @@ Proof.
 Qed.
 
 Lemma AtomicSeen_join l γ ζ ζ' :
-  l sn⊒{γ} ζ -∗ l sn⊒{γ} ζ' -∗ l sn⊒{γ} (ζ ∪ ζ').
+  l sn⊒{γ} ζ ⊢ l sn⊒{γ} ζ' -∗ l sn⊒{γ} (ζ ∪ ζ').
 Proof.
   rewrite AtomicSeen_eq. iIntros "(SL1 & SR1 & Va1) (SL2 & SR2 & Va2)".
   iDestruct "Va1" as (Va) "(% & NL & Va1)".
@@ -626,30 +626,30 @@ Lemma AtomicSeen_join' l γ ζ ζ' :
 Proof. apply bi.wand_elim_l', AtomicSeen_join. Qed.
 
 Lemma AtomicPtsToX_AtomicSeen_latest l γ t ζ ζ' m V V' :
-  @{V} AtomicPtsToX l γ t ζ m -∗ @{V'} l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsToX l γ t ζ m ⊢ @{V'} l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof.
   rewrite AtomicPtsToX_eq AtomicSeen_eq.
   iDestruct 1 as (?????) "(_&_&_&_&SA&_)". iIntros "(_ & R & _)".
   by iDestruct (at_auth_reader_latest with "[$SA] [$R]") as %?.
 Qed.
 Lemma AtomicPtsToX_AtomicSeen_latest_1 l γ t ζ ζ' m V :
-  @{V} AtomicPtsToX l γ t ζ m -∗ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsToX l γ t ζ m ⊢ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_r, AtomicPtsToX_AtomicSeen_latest. Qed.
 Lemma AtomicPtsToX_AtomicSeen_latest_2 l γ t ζ ζ' m :
-  AtomicPtsToX l γ t ζ m -∗ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  AtomicPtsToX l γ t ζ m ⊢ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_lr, AtomicPtsToX_AtomicSeen_latest. Qed.
 
 Lemma AtomicPtsTo_AtomicSeen_latest l γ ζ ζ' m V V' :
-  @{V} AtomicPtsTo l γ ζ m -∗ @{V'} l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsTo l γ ζ m ⊢ @{V'} l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof.
   rewrite AtomicPtsTo_eq view_at_exist. apply bi.exist_elim => ?.
   by apply AtomicPtsToX_AtomicSeen_latest.
 Qed.
 Lemma AtomicPtsTo_AtomicSeen_latest_1 l γ ζ ζ' m V :
-  @{V} AtomicPtsTo l γ ζ m -∗ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsTo l γ ζ m ⊢ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_r, AtomicPtsTo_AtomicSeen_latest. Qed.
 Lemma AtomicPtsTo_AtomicSeen_latest_2 l γ ζ ζ' m :
-  AtomicPtsTo l γ ζ m -∗ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  AtomicPtsTo l γ ζ m ⊢ l sn⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_lr, AtomicPtsTo_AtomicSeen_latest. Qed.
 
 Lemma AtomicSeen_union_equiv l γ ζ1 ζ2 V1 V2 :
@@ -707,7 +707,7 @@ Qed.
 
 Lemma AtomicSeen_AtomicSync_singleton l γ t v V :
   let ζ := {[t := (v, V)]} in
-  ⊒V -∗ l sn⊒{γ} ζ -∗ l sy⊒{γ} ζ.
+  ⊒V ⊢ l sn⊒{γ} ζ -∗ l sy⊒{γ} ζ.
 Proof.
   rewrite AtomicSync_eq AtomicSeen_eq /AtomicSync_def /AtomicSeen_def.
   iIntros "SV [SL $]".
@@ -715,7 +715,7 @@ Proof.
 Qed.
 
 Lemma AtomicPtsToX_AtomicSync l γ t ζ m :
-  AtomicPtsToX l γ t ζ m -∗ l sy⊒{γ} ζ.
+  AtomicPtsToX l γ t ζ m ⊢ l sy⊒{γ} ζ.
 Proof.
   rewrite AtomicPtsToX_eq AtomicSync_eq.
   iDestruct 1 as (?????) "(F & ($ & ? & ? & NL) & ? & ? & (W & SW & NA) & _)".
@@ -726,17 +726,17 @@ Proof.
     move => EqE. move : IS. by rewrite EqE => [[?]].
 Qed.
 Lemma AtomicPtsToX_AtomicSeen l γ t ζ m :
-  AtomicPtsToX l γ t ζ m -∗ l sn⊒{γ} ζ.
+  AtomicPtsToX l γ t ζ m ⊢ l sn⊒{γ} ζ.
 Proof. rewrite AtomicPtsToX_AtomicSync. by apply AtomicSync_AtomicSeen. Qed.
 
 Lemma AtomicPtsTo_AtomicSync l γ ζ m :
-  AtomicPtsTo l γ ζ m -∗ l sy⊒{γ} ζ.
+  AtomicPtsTo l γ ζ m ⊢ l sy⊒{γ} ζ.
 Proof.
   rewrite AtomicPtsTo_eq. apply bi.exist_elim => ?.
   by apply AtomicPtsToX_AtomicSync.
 Qed.
 Lemma AtomicPtsTo_AtomicSeen l γ ζ m :
-  AtomicPtsTo l γ ζ m -∗ l sn⊒{γ} ζ.
+  AtomicPtsTo l γ ζ m ⊢ l sn⊒{γ} ζ.
 Proof. rewrite AtomicPtsTo_AtomicSync. by apply AtomicSync_AtomicSeen. Qed.
 
 Lemma AtomicSync_join l γ ζ ζ' :
@@ -753,56 +753,56 @@ Proof.
 Qed.
 
 Lemma AtomicPtsTo_AtomicSync_latest l γ ζ ζ' m V V' :
-  @{V} AtomicPtsTo l γ ζ m -∗ @{V'} l sy⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsTo l γ ζ m ⊢ @{V'} l sy⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof.
   iIntros "P C". iApply (AtomicPtsTo_AtomicSeen_latest with "P").
   by rewrite AtomicSync_AtomicSeen.
 Qed.
 Lemma AtomicPtsTo_AtomicSync_latest_1 l γ ζ ζ' m V :
-  @{V} AtomicPtsTo l γ ζ m -∗ l sy⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsTo l γ ζ m ⊢ l sy⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_r, AtomicPtsTo_AtomicSync_latest. Qed.
 Lemma AtomicPtsTo_AtomicSync_latest_2 l γ ζ ζ' m :
-  AtomicPtsTo l γ ζ m -∗ l sy⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  AtomicPtsTo l γ ζ m ⊢ l sy⊒{γ} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_lr, AtomicPtsTo_AtomicSync_latest. Qed.
 
 (* AtomicSWriter *)
-Lemma AtomicSWriter_AtomicSync l γ ζ : l sw⊒{γ} ζ -∗ l sy⊒{γ} ζ.
+Lemma AtomicSWriter_AtomicSync l γ ζ : l sw⊒{γ} ζ ⊢ l sy⊒{γ} ζ.
 Proof. rewrite AtomicSWriter_eq. iDestruct 1 as "([$ _] & _)". Qed.
 
-Lemma AtomicSWriter_AtomicSeen l γ ζ : l sw⊒{γ} ζ -∗ l sn⊒{γ} ζ.
+Lemma AtomicSWriter_AtomicSeen l γ ζ : l sw⊒{γ} ζ ⊢ l sn⊒{γ} ζ.
 Proof. rewrite -AtomicSync_AtomicSeen. by apply AtomicSWriter_AtomicSync. Qed.
 
 Lemma AtomicSWriter_exclusive_obj l γ ζ1 ζ2 V1 V2:
-  @{V1} l sw⊒{γ} ζ1 -∗ @{V2} l sw⊒{γ} ζ2 -∗ False.
+  @{V1} l sw⊒{γ} ζ1 ⊢ @{V2} l sw⊒{γ} ζ2 -∗ False.
 Proof.
   rewrite AtomicSWriter_eq. iIntros "[[_ W1] _] [[_ W2] _]".
   by iDestruct (at_writer_exclusive with "[$W1] [$W2]") as %?.
 Qed.
 Lemma AtomicSWriter_exclusive l γ ζ1 ζ2 :
-  l sw⊒{γ} ζ1 -∗ l sw⊒{γ} ζ2 -∗ False.
+  l sw⊒{γ} ζ1 ⊢ l sw⊒{γ} ζ2 -∗ False.
 Proof. apply view_at_wand_lr, AtomicSWriter_exclusive_obj. Qed.
 
 Lemma at_writer_AtomicSeen_latest l γ ζ1 ζ2 V2 :
-  ⎡ at_writer γ ζ2 ⎤ -∗ @{V2} l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
+  ⎡ at_writer γ ζ2 ⎤ ⊢ @{V2} l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
 Proof.
   rewrite AtomicSeen_eq. iIntros "W (_ & R & _)".
   by iDestruct (at_writer_latest with "W [$R]") as %?.
 Qed.
 Lemma at_writer_AtomicSeen_latest_1 l γ ζ1 ζ2 :
-  ⎡ at_writer γ ζ2 ⎤ -∗ l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
+  ⎡ at_writer γ ζ2 ⎤ ⊢ l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
 Proof.
   apply view_at_wand_lr. intros. rewrite view_at_objective_iff.
   by apply at_writer_AtomicSeen_latest.
 Qed.
 
 Lemma AtomicSWriter_latest_obj l γ ζ1 ζ2 V1 V2 :
-  @{V1} l sw⊒{γ} ζ2 -∗ @{V2} l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
+  @{V1} l sw⊒{γ} ζ2 ⊢ @{V2} l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
 Proof.
   rewrite AtomicSWriter_eq. iIntros "[[_ W] _]".
   iApply (at_writer_AtomicSeen_latest with "[$W]").
 Qed.
 Lemma AtomicSWriter_latest l γ ζ1 ζ2 :
-  l sw⊒{γ} ζ2 -∗ l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
+  l sw⊒{γ} ζ2 ⊢ l sn⊒{γ} ζ1 -∗ ⌜ζ1 ⊆ ζ2⌝.
 Proof. apply view_at_wand_lr, AtomicSWriter_latest_obj. Qed.
 
 Lemma AtomicSWriter_AtomicPtsToX_NonSW_excluded_obj
@@ -817,35 +817,35 @@ Qed.
 
 Lemma AtomicSWriter_AtomicPtsToX_is_SW
   l γ ζ1 t2 ζ2 mode V1 V2 :
-  @{V1} l sw⊒{γ} ζ1 -∗ @{V2} AtomicPtsToX l γ t2 ζ2 mode -∗ ⌜ mode = SingleWriter ⌝.
+  @{V1} l sw⊒{γ} ζ1 ⊢ @{V2} AtomicPtsToX l γ t2 ζ2 mode -∗ ⌜ mode = SingleWriter ⌝.
 Proof.
   iIntros "W P". destruct mode; [done|..];
     by iDestruct (AtomicSWriter_AtomicPtsToX_NonSW_excluded_obj with "W P") as %?.
 Qed.
 Lemma AtomicSWriter_AtomicPtsToX_is_SW_1
   l γ ζ1 t2 ζ2 mode V2 :
-  l sw⊒{γ} ζ1 -∗ @{V2} AtomicPtsToX l γ t2 ζ2 mode -∗ ⌜ mode = SingleWriter ⌝.
+  l sw⊒{γ} ζ1 ⊢ @{V2} AtomicPtsToX l γ t2 ζ2 mode -∗ ⌜ mode = SingleWriter ⌝.
 Proof. by apply view_at_wand_l, AtomicSWriter_AtomicPtsToX_is_SW. Qed.
 Lemma AtomicSWriter_AtomicPtsToX_is_SW_2
   l γ ζ1 t2 ζ2 mode :
-  l sw⊒{γ} ζ1 -∗ AtomicPtsToX l γ t2 ζ2 mode -∗ ⌜ mode = SingleWriter ⌝.
+  l sw⊒{γ} ζ1 ⊢ AtomicPtsToX l γ t2 ζ2 mode -∗ ⌜ mode = SingleWriter ⌝.
 Proof. by apply view_at_wand_lr, AtomicSWriter_AtomicPtsToX_is_SW. Qed.
 
 
 Lemma AtomicSWriter_AtomicPtsTo_NonSW_excluded_obj
   l γ ζ1 ζ2 mode (NSW: mode ≠ SingleWriter) V1 V2 :
-  @{V1} l sw⊒{γ} ζ1 -∗ @{V2} AtomicPtsTo l γ ζ2 mode -∗ False.
+  @{V1} l sw⊒{γ} ζ1 ⊢ @{V2} AtomicPtsTo l γ ζ2 mode -∗ False.
 Proof.
   rewrite AtomicPtsTo_eq. iIntros "H1 [% H2]".
   by iApply (AtomicSWriter_AtomicPtsToX_NonSW_excluded_obj with "H1 H2").
 Qed.
 Lemma AtomicSWriter_AtomicPtsTo_NonSW_excluded
   l γ ζ1 ζ2 mode (NSW: mode ≠ SingleWriter) :
-  l sw⊒{γ} ζ1 -∗ AtomicPtsTo l γ ζ2 mode -∗ False.
+  l sw⊒{γ} ζ1 ⊢ AtomicPtsTo l γ ζ2 mode -∗ False.
 Proof. by apply view_at_wand_lr, AtomicSWriter_AtomicPtsTo_NonSW_excluded_obj. Qed.
 
 Lemma AtomicSWriter_CASerX_excluded l γ ζ1 ζ2 t q2 V1 V2 :
-  @{V1} l sw⊒{γ} ζ1 -∗ @{V2} l casX⊒{γ,t,q2} ζ2 -∗ False.
+  @{V1} l sw⊒{γ} ζ1 ⊢ @{V2} l casX⊒{γ,t,q2} ζ2 -∗ False.
 Proof.
   rewrite AtomicSWriter_eq AtomicCASerX_eq.
   iIntros "[_ [% [E1 _]]] [_ [E2 _]]".
@@ -853,10 +853,10 @@ Proof.
     as %[?%Qp.not_add_le_l _].
 Qed.
 Lemma AtomicSWriter_CASerX_excluded_1 l γ ζ1 ζ2 t q2 V2 :
-  l sw⊒{γ} ζ1 -∗ @{V2} l casX⊒{γ,t,q2} ζ2 -∗ False.
+  l sw⊒{γ} ζ1 ⊢ @{V2} l casX⊒{γ,t,q2} ζ2 -∗ False.
 Proof. apply view_at_wand_l, AtomicSWriter_CASerX_excluded. Qed.
 Lemma AtomicSWriter_CASerX_excluded_2 l γ ζ1 ζ2 t q2 :
-  l sw⊒{γ} ζ1 -∗ l casX⊒{γ,t,q2} ζ2 -∗ False.
+  l sw⊒{γ} ζ1 ⊢ l casX⊒{γ,t,q2} ζ2 -∗ False.
 Proof. apply view_at_wand_lr, AtomicSWriter_CASerX_excluded. Qed.
 
 Lemma AtomicPtsToX_at_writer_agree l γ t1 ζ1 ζ2 mode V1 :
@@ -867,42 +867,42 @@ Proof.
 Qed.
 
 Lemma AtomicPtsToX_SWriter_agree l γ t1 ζ1 ζ2 mode V1 V2 :
-  @{V1}(AtomicPtsToX l γ t1 ζ1 mode) -∗ @{V2} l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
+  @{V1}(AtomicPtsToX l γ t1 ζ1 mode) ⊢ @{V2} l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
 Proof.
   rewrite AtomicSWriter_eq. iIntros "P [[_ W] _]".
   iApply (AtomicPtsToX_at_writer_agree with "P [$W]").
 Qed.
 Lemma AtomicPtsToX_AtomicSWriter_agree_1 l γ t1 ζ1 ζ2 mode V1 :
-  @{V1}(AtomicPtsToX l γ t1 ζ1 mode) -∗ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
+  @{V1}(AtomicPtsToX l γ t1 ζ1 mode) ⊢ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
 Proof. apply view_at_wand_r, AtomicPtsToX_SWriter_agree. Qed.
 Lemma AtomicPtsToX_AtomicSWriter_agree_2 l γ t1 ζ1 ζ2 mode :
-  AtomicPtsToX l γ t1 ζ1 mode -∗ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
+  AtomicPtsToX l γ t1 ζ1 mode ⊢ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
 Proof. apply view_at_wand_lr, AtomicPtsToX_SWriter_agree. Qed.
 
 Lemma AtomicPtsTo_SWriter_agree l γ ζ1 ζ2 mode V1 V2 :
-  @{V1}(AtomicPtsTo l γ ζ1 mode) -∗ @{V2} l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
+  @{V1}(AtomicPtsTo l γ ζ1 mode) ⊢ @{V2} l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
 Proof.
   rewrite AtomicPtsTo_eq view_at_exist. apply bi.exist_elim => ?.
   by apply AtomicPtsToX_SWriter_agree.
 Qed.
 Lemma AtomicPtsTo_AtomicSWriter_agree_1 l γ ζ1 ζ2 mode V1 :
-  @{V1}(AtomicPtsTo l γ ζ1 mode) -∗ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
+  @{V1}(AtomicPtsTo l γ ζ1 mode) ⊢ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
 Proof. apply view_at_wand_r, AtomicPtsTo_SWriter_agree. Qed.
 Lemma AtomicPtsTo_AtomicSWriter_agree_2 l γ ζ1 ζ2 mode :
-  AtomicPtsTo l γ ζ1 mode -∗ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
+  AtomicPtsTo l γ ζ1 mode ⊢ l sw⊒{γ} ζ2 -∗ ⌜ζ1 = ζ2⌝.
 Proof. apply view_at_wand_lr, AtomicPtsTo_SWriter_agree. Qed.
 
 (* AtomicCASer *)
-Lemma AtomicCASerX_AtomicSeen l γ t ζ q : l casX⊒{γ,t,q} ζ -∗ l sn⊒{γ} ζ.
+Lemma AtomicCASerX_AtomicSeen l γ t ζ q : l casX⊒{γ,t,q} ζ ⊢ l sn⊒{γ} ζ.
 Proof. rewrite AtomicCASerX_eq. by iIntros "[$ _]". Qed.
-Lemma AtomicCASer_AtomicSeen l γ ζ q : l cas⊒{γ,q} ζ -∗ l sn⊒{γ} ζ.
+Lemma AtomicCASer_AtomicSeen l γ ζ q : l cas⊒{γ,q} ζ ⊢ l sn⊒{γ} ζ.
 Proof.
   rewrite AtomicCASer_eq. apply bi.exist_elim => ?.
   apply : AtomicCASerX_AtomicSeen.
 Qed.
 
 Lemma AtomicPtsToX_AtomicCASerX_latest l γ t ζ t' ζ' m q V V' :
-  @{V} AtomicPtsToX l γ t ζ m -∗ @{V'} l casX⊒{γ,t',q} ζ' -∗ ⌜ t' = t ∧ ζ' ⊆ ζ ⌝.
+  @{V} AtomicPtsToX l γ t ζ m ⊢ @{V'} l casX⊒{γ,t',q} ζ' -∗ ⌜ t' = t ∧ ζ' ⊆ ζ ⌝.
 Proof.
   rewrite AtomicCASerX_eq. iIntros "P [S [SW _]]".
   iDestruct (AtomicPtsToX_AtomicSeen_latest with  "P S") as %?.
@@ -911,23 +911,23 @@ Proof.
   by iDestruct (at_full_auth_exclusive_write_agree with "[$SA] [$SW]") as %<-.
 Qed.
 Lemma AtomicPtsToX_AtomicCASerX_latest_1 l γ t ζ t' ζ' m q V :
-  @{V} AtomicPtsToX l γ t ζ m -∗ l casX⊒{γ,t',q} ζ' -∗ ⌜ t' = t ∧ ζ' ⊆ ζ ⌝.
+  @{V} AtomicPtsToX l γ t ζ m ⊢ l casX⊒{γ,t',q} ζ' -∗ ⌜ t' = t ∧ ζ' ⊆ ζ ⌝.
 Proof. apply view_at_wand_r, AtomicPtsToX_AtomicCASerX_latest. Qed.
 Lemma AtomicPtsToX_AtomicCASerX_latest_2 l γ t ζ t' ζ' m q :
-  AtomicPtsToX l γ t ζ m -∗ l casX⊒{γ,t', q} ζ' -∗ ⌜ t' = t ∧ ζ' ⊆ ζ ⌝.
+  AtomicPtsToX l γ t ζ m ⊢ l casX⊒{γ,t', q} ζ' -∗ ⌜ t' = t ∧ ζ' ⊆ ζ ⌝.
 Proof. apply view_at_wand_lr, AtomicPtsToX_AtomicCASerX_latest. Qed.
 
 Lemma AtomicPtsTo_AtomicCASer_latest l γ ζ ζ' m q V V' :
-  @{V} AtomicPtsTo l γ ζ m -∗ @{V'} l cas⊒{γ,q} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsTo l γ ζ m ⊢ @{V'} l cas⊒{γ,q} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof.
   iIntros "P C". iApply (AtomicPtsTo_AtomicSeen_latest with "P").
   by rewrite AtomicCASer_AtomicSeen.
 Qed.
 Lemma AtomicPtsTo_AtomicCASer_latest_1 l γ ζ ζ' m q V :
-  @{V} AtomicPtsTo l γ ζ m -∗ l cas⊒{γ,q} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  @{V} AtomicPtsTo l γ ζ m ⊢ l cas⊒{γ,q} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_r, AtomicPtsTo_AtomicCASer_latest. Qed.
 Lemma AtomicPtsTo_AtomicCASer_latest_2 l γ ζ ζ' m q :
-  AtomicPtsTo l γ ζ m -∗ l cas⊒{γ,q} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
+  AtomicPtsTo l γ ζ m ⊢ l cas⊒{γ,q} ζ' -∗ ⌜ζ' ⊆ ζ⌝.
 Proof. apply view_at_wand_lr, AtomicPtsTo_AtomicCASer_latest. Qed.
 
 Lemma AtomicCASerX_AtomicPtsToX_is_not_concurrent
@@ -962,7 +962,7 @@ Proof.
 Qed.
 
 Lemma AtomicCASerXs_join l γ t1 t2 ζ1 ζ2 q1 q2 :
-  l casX⊒{γ,t1,q1} ζ1 -∗ l casX⊒{γ,t2,q2} ζ2 -∗ l casX⊒{γ,t1,q1 + q2} (ζ1 ∪ ζ2).
+  l casX⊒{γ,t1,q1} ζ1 ⊢ l casX⊒{γ,t2,q2} ζ2 -∗ l casX⊒{γ,t1,q1 + q2} (ζ1 ∪ ζ2).
 Proof.
   rewrite AtomicCASerX_eq.
   iIntros "[S1 [SW [%vV %IS]]] [S2 [SW' %]]".
@@ -989,7 +989,7 @@ Proof.
 Qed.
 
 Lemma AtomicCASer_AtomicSeen_update_join l γ ζ q ζ' :
-  l cas⊒{γ,q} ζ -∗ l sn⊒{γ} ζ' -∗ l cas⊒{γ,q} (ζ ∪ ζ').
+  l cas⊒{γ,q} ζ ⊢ l sn⊒{γ} ζ' -∗ l cas⊒{γ,q} (ζ ∪ ζ').
 Proof.
   rewrite AtomicCASer_eq. iIntros "[%tx C] S". iExists tx.
   by iApply (AtomicCASerX_AtomicSeen_update_join with "C S").
@@ -1006,7 +1006,7 @@ Qed.
 
 (* CAS and CON *)
 Lemma AtomicPtsToX_SW_max_time l γ tx ζ m V1 V2 :
-  @{V1} AtomicPtsToX l γ tx ζ m -∗ @{V2} l sw⊒{γ} ζ -∗ ⌜ max_time tx ζ ⌝.
+  @{V1} AtomicPtsToX l γ tx ζ m ⊢ @{V2} l sw⊒{γ} ζ -∗ ⌜ max_time tx ζ ⌝.
 Proof.
   rewrite AtomicPtsToX_eq /AtomicPtsToX_def AtomicSWriter_eq /AtomicSWriter_def.
   iDestruct 1 as (C Va rsa rns ws) "(_ & _ & _ & _ & A & _)".
@@ -1014,7 +1014,7 @@ Proof.
   by iDestruct (at_full_auth_exclusive_write_agree with "[$A] [$Ex]") as %<-.
 Qed.
 Lemma AtomicPtsToX_SW_max_time_1 l γ tx ζ m V1 :
-  @{V1} AtomicPtsToX l γ tx ζ m -∗ l sw⊒{γ} ζ -∗ ⌜ max_time tx ζ ⌝.
+  @{V1} AtomicPtsToX l γ tx ζ m ⊢ l sw⊒{γ} ζ -∗ ⌜ max_time tx ζ ⌝.
 Proof. by apply view_at_wand_r, AtomicPtsToX_SW_max_time. Qed.
 
 Lemma AtomicPtsToX_is_SomeX l γ tx ζ m :
@@ -1261,9 +1261,9 @@ Proof.
 Qed.
 
 Lemma AtomicPtsTo_CON_to_SW l γ ζ :
-  l at↦{γ} ζ ==∗ l sw↦{γ} ζ ∗ l sw⊒{γ} ζ.
+  l at↦{γ} ζ ⊢ |==> l sw↦{γ} ζ ∗ l sw⊒{γ} ζ.
 Proof.
-  rewrite AtomicPtsTo_CON_CAS_1. apply bi.wand_elim_l', AtomicPtsTo_CAS_to_SW_1.
+  rewrite AtomicPtsTo_CON_CAS_1. apply bi.wand_elim_l', bi.wand_entails, AtomicPtsTo_CAS_to_SW_1.
 Qed.
 
 (* From and to non-atomic pointsto *)
@@ -1284,7 +1284,7 @@ Proof.
 Qed.
 
 Lemma from_own_loc_na l q v Vinit :
-  ⊒Vinit -∗ l ↦{q} v -∗
+  ⊒Vinit ⊢ l ↦{q} v -∗
   ∃ t m rsa ws rsn Va,
   let C := {[t := m]} in
   ⌜good_hist C ∧ memval_val_rel m.(mval) v ∧ Vinit ⊑ Va⌝ ∗
@@ -1414,7 +1414,7 @@ Proof.
 Qed.
 
 Lemma AtomicPtsToX_from_na_cofinite_rel_view l v (G : gset gname) P :
-  P -∗ l ↦ v ==∗
+  P ⊢ l ↦ v ==∗
   ∃ γ t V, ⌜γ ∉ G⌝ ∗ ⊒V ∗ @{V} P ∗
            let ζ := {[t := (v,V)]} in @{V} l sw⊒{γ} ζ ∗ @{V} l swX↦{γ,t} ζ.
 Proof.
@@ -1425,7 +1425,7 @@ Proof.
   iIntros "!>". iExists γ, t, V. by iFrame (FR) "sV P Pts".
 Qed.
 Lemma AtomicPtsToX_from_na_cofinite_rel l v (G : gset gname) P :
-  P -∗ l ↦ v ==∗ ∃ γ t V, ⌜γ ∉ G⌝ ∗ ⊒V ∗ @{V} P ∗
+  P ⊢ l ↦ v ==∗ ∃ γ t V, ⌜γ ∉ G⌝ ∗ ⊒V ∗ @{V} P ∗
                   let ζ := {[t := (v,V)]} in l sw⊒{γ} ζ ∗ l swX↦{γ,t} ζ.
 Proof.
   iIntros "P NA".
@@ -1445,7 +1445,7 @@ Proof.
   iIntros "!>". iExists γ, t, V. by iFrame.
 Qed.
 Lemma AtomicPtsToX_from_na_rel_view l v P :
-  P -∗ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
+  P ⊢ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
             let ζ := {[t := (v,V)]} in @{V} l sw⊒{γ} ζ ∗ @{V} l swX↦{γ,t} ζ.
 Proof.
   iIntros "P N".
@@ -1454,7 +1454,7 @@ Proof.
   iIntros "!>". iExists γ, t, V. by iFrame.
 Qed.
 Lemma AtomicPtsToX_from_na_rel l v P :
-  P -∗ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
+  P ⊢ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
             let ζ := {[t := (v,V)]} in l sw⊒{γ} ζ ∗ l swX↦{γ,t} ζ.
 Proof.
   iIntros "P N".
@@ -1466,12 +1466,12 @@ Lemma AtomicPtsToX_from_na l v :
   l ↦ v ==∗ ∃ γ t V, ⊒V ∗
             let ζ := {[t := (v,V)]} in l sw⊒{γ} ζ ∗ l swX↦{γ,t} ζ.
 Proof.
-  rewrite (AtomicPtsToX_from_na_cofinite l v ∅). apply bupd_mono.
-  iDestruct 1 as (γ t V) "[_ E]". eauto.
+  iIntros "P". iMod (AtomicPtsToX_from_na_cofinite _ _ ∅ with "P") as "P".
+  iDestruct "P" as (γ t V) "[_ E]". eauto.
 Qed.
 
 Lemma AtomicPtsTo_from_na_cofinite_rel l v (G : gset gname) P :
-  P -∗ l ↦ v ==∗ ∃ γ t V, ⌜γ ∉ G⌝ ∗ ⊒V ∗ @{V} P ∗
+  P ⊢ l ↦ v ==∗ ∃ γ t V, ⌜γ ∉ G⌝ ∗ ⊒V ∗ @{V} P ∗
                   let ζ := {[t := (v,V)]} in l sw⊒{γ} ζ ∗ l sw↦{γ} ζ.
 Proof.
   iIntros "P NA". rewrite AtomicPtsTo_eq.
@@ -1489,7 +1489,7 @@ Proof.
   iIntros "!>". iExists γ, t, V. by iFrame.
 Qed.
 Lemma AtomicPtsTo_from_na_rel l v P :
-  P -∗ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
+  P ⊢ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
             let ζ := {[t := (v,V)]} in l sw⊒{γ} ζ ∗ l sw↦{γ} ζ.
 Proof.
   iIntros "P N".
@@ -1501,12 +1501,12 @@ Lemma AtomicPtsTo_from_na l v :
   l ↦ v ==∗ ∃ γ t V, ⊒V ∗
             let ζ := {[t := (v,V)]} in l sw⊒{γ} ζ ∗ l sw↦{γ} ζ.
 Proof.
-  rewrite (AtomicPtsTo_from_na_cofinite l v ∅). apply bupd_mono.
-  iDestruct 1 as (γ t V) "[_ E]". eauto.
+  iIntros "P". iMod (AtomicPtsTo_from_na_cofinite l v ∅ with "P") as "P".
+  iDestruct "P" as (γ t V) "[_ E]". eauto.
 Qed.
 
 Lemma AtomicPtsTo_CON_from_na_cofinite_rel l v (G : gset gname) P :
-  P -∗ l ↦ v ==∗ ∃ γ t V, ⌜γ ∉ G⌝ ∗ ⊒V ∗ @{V} P ∗
+  P ⊢ l ↦ v ==∗ ∃ γ t V, ⌜γ ∉ G⌝ ∗ ⊒V ∗ @{V} P ∗
                           let ζ := {[t := (v,V)]} in l sn⊒{γ} ζ ∗ l at↦{γ} ζ.
 Proof.
   iIntros "P NA".
@@ -1528,7 +1528,7 @@ Proof.
 Qed.
 
 Lemma AtomicPtsTo_CON_from_na_rel l v P :
-  P -∗ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
+  P ⊢ l ↦ v ==∗ ∃ γ t V, ⊒V ∗ @{V} P ∗
   let ζ := {[t := (v,V)]} in l sn⊒{γ} ζ ∗ l at↦{γ} ζ.
 Proof.
   iIntros "P NA".
@@ -1541,8 +1541,8 @@ Lemma AtomicPtsTo_CON_from_na l v :
   l ↦ v ==∗ ∃ γ t V, ⊒V ∗
   let ζ := {[t := (v,V)]} in l sn⊒{γ} ζ ∗ l at↦{γ} ζ.
 Proof.
-  rewrite (AtomicPtsTo_CON_from_na_cofinite l v ∅). apply bupd_mono.
-  iDestruct 1 as (γ t V) "[_ E]". eauto.
+  iIntros "P". iMod (AtomicPtsTo_CON_from_na_cofinite l v ∅ with "P") as "P".
+  iDestruct "P" as (γ t V) "[_ E]". eauto.
 Qed.
 End props.
 
diff --git a/gpfsl/logic/invariants.v b/gpfsl/logic/invariants.v
index 78fcaf695748a8c4fdce30a9362c4a03a78bc08c..95c203f2e6593c26b359043d186388b822cc7279 100644
--- a/gpfsl/logic/invariants.v
+++ b/gpfsl/logic/invariants.v
@@ -82,7 +82,7 @@ Proof.
 Qed.
 
 Lemma inv_alloc N E P `{!Objective P} : ▷ P ={E}=∗ inv N P.
-Proof. by rewrite -inv_alloc' -objective_objectively. Qed.
+Proof. iIntros "?". iApply inv_alloc'. iApply objective_objectively. done. Qed.
 
 Lemma inv_alloc_open N E P `{!Objective P} :
   ↑N ⊆ E → ⊢ |={E, E∖↑N}=> inv N P ∗ (▷ P ={E∖↑N, E}=∗ True).
diff --git a/gpfsl/logic/lifting.v b/gpfsl/logic/lifting.v
index b94837b5fd2c88c0636f8902e39e89ec30fc7100..36f0b2b2d7dde8ab9a445a0a3ae6bf2fac9c28b3 100644
--- a/gpfsl/logic/lifting.v
+++ b/gpfsl/logic/lifting.v
@@ -19,7 +19,7 @@ Implicit Types (E : coPset) (e : expr) (v : val) (Φ : val → vProp Σ) (tid :
 
 Lemma wp_bind {tid E e} K Φ (SUB: ↑histN ⊆ E) :
   WP e @ tid; E {{ v, WP fill K (of_val v) @ tid; E {{ Φ }} }}
-  -∗ WP fill K e @ tid; E {{ Φ }}.
+  ⊢ WP fill K e @ tid; E {{ Φ }}.
 Proof. (* in iProp *)
   constructor => ?. rewrite wp_eq /wp_def /=.
   iIntros "WP" (𝓥 Ext) "H𝓥 #s".
@@ -31,7 +31,7 @@ Proof. (* in iProp *)
 Qed.
 
 Lemma wp_bindi {tid E e} Ki Φ (SUB: ↑histN ⊆ E) :
-  WP e @ tid; E {{ v, WP fill_item Ki (of_val v) @ tid; E {{ Φ }} }} -∗
+  WP e @ tid; E {{ v, WP fill_item Ki (of_val v) @ tid; E {{ Φ }} }} ⊢
   WP fill_item Ki e @ tid; E {{ Φ }}.
 Proof. (* in iProp *)
   constructor => ?. rewrite wp_eq /wp_def /=.
@@ -179,7 +179,7 @@ Qed.
 Lemma wp_write_non_atomic l v tid E:
   ↑histN ⊆ E → {{{ l ↦ ? }}} #l <- v @ tid; E {{{ RET #☠; l ↦ v }}}.
 Proof. (* in iProp *)
-  iIntros (? Φ). constructor => ?.
+  iIntros (? Φ). apply bi.entails_wand. constructor => ?.
   iIntros "own" (V ?) "Post". rewrite wp_eq /wp_def. iIntros (??) "H𝓥 s".
   iApply iwp_fupd. iApply (iwp_write_non_atomic with "[$s $own]"); [done..|].
   iNext. iIntros (𝓥') "(% & ? & ?)".
@@ -191,7 +191,7 @@ Qed.
 Lemma wp_write_atomic l v o tid E (HRLX: Relaxed ⊑ o) :
   ↑histN ⊆ E → {{{ l ↦ ? }}} Write o #l v @ tid; E {{{ RET #☠; l ↦ v }}}.
 Proof.
-  iIntros (? Φ). constructor => ?.
+  iIntros (? Φ). apply bi.entails_wand. constructor => ?.
   iIntros "own" (? ->) "Post". iApply wp_hist_inv; [done|]. iIntros (? ->) "#HInv".
   rewrite wp_eq /wp_def. iIntros (𝓥 ->) "H𝓥 s".
   iApply iwp_fupd. rewrite own_loc_eq.
@@ -242,7 +242,7 @@ Qed.
    taking a step *)
 
 Lemma wp_rel_revert_view_at (P : vProp Σ) e tid E Φ :
-  △{tid} P -∗
+  △{tid} P ⊢
   (∀ V : view, △{tid} (⊒V) -∗ @{V} P -∗ ⊒V -∗ WP e @ tid; E {{ Φ }}) -∗
   WP e @ tid; E {{ Φ }}.
 Proof.
@@ -267,7 +267,7 @@ Proof.
 Qed.
 
 Lemma wp_rel_fence_intro (P : vProp Σ) tid E Φ (SUB: ↑histN ⊆ E):
-  P -∗ WP FenceRel @ tid; E {{ v, △{tid} P -∗ Φ v }}
+  P ⊢ WP FenceRel @ tid; E {{ v, △{tid} P -∗ Φ v }}
     -∗ WP FenceRel @ tid; E {{ v, Φ v }}.
 Proof.
   constructor => V. iIntros "P" (? Ext0) "WP".
@@ -321,7 +321,7 @@ Qed.
 
 (** Acquire fences *)
 Lemma wp_acq_intro (P : vProp Σ) e tid E Φ :
-  P -∗
+  P ⊢
   (▽{tid} P -∗ WP e @ tid; E {{ Φ }}) -∗
   WP e @ tid; E {{ Φ }}.
 Proof.
@@ -334,7 +334,7 @@ Proof.
 Qed.
 
 Lemma wp_acq_fence_elim (P : vProp Σ) tid E Φ (SUB: ↑histN ⊆ E):
-  ▽{tid} P -∗ WP FenceAcq @ tid; E {{ v, P -∗ Φ v }}
+  ▽{tid} P ⊢ WP FenceAcq @ tid; E {{ v, P -∗ Φ v }}
   -∗ WP FenceAcq @ tid; E {{ v, Φ v }}.
 Proof.
   constructor => ?. iIntros "AP" (V ->) "WP". rewrite wp_eq /wp_def /=.
@@ -386,7 +386,7 @@ Qed.
 
 (** SC fences *)
 Lemma wp_sc_fence_rel_intro (P : vProp Σ) tid E Φ (SUB: ↑histN ⊆ E):
-  P -∗ WP FenceSC @ tid; E {{ v, △{tid} P -∗ Φ v }}
+  P ⊢ WP FenceSC @ tid; E {{ v, △{tid} P -∗ Φ v }}
   -∗ WP FenceSC @ tid; E {{ v, Φ v }}.
 Proof.
   constructor => V. iIntros "P" (? Ext0) "WP".
@@ -439,7 +439,7 @@ Proof.
 Qed.
 
 Lemma wp_sc_fence_acq_elim (P : vProp Σ) tid E Φ (SUB: ↑histN ⊆ E):
-  ▽{tid} P -∗ WP FenceSC @ tid; E {{ v, P -∗ Φ v }}
+  ▽{tid} P ⊢ WP FenceSC @ tid; E {{ v, P -∗ Φ v }}
   -∗ WP FenceSC @ tid; E {{ v, Φ v }}.
 Proof.
   constructor => ?. iIntros "AP" (V ->) "WP".
@@ -494,10 +494,10 @@ Qed.
 
 (** Pointer comparison *)
 Lemma wp_eq_loc tid E (l1 l2 : loc) q1 q2 P Φ (SUB: ↑histN ⊆ E):
-  (P -∗ ▷ l1 ↦{q1} ?) →
-  (P -∗ ▷ l2 ↦{q2} ?) →
-  (P -∗ ▷ Φ (#(bool_decide (l1 = l2)))) →
-  P -∗ WP #l1 = #l2 @ tid; E {{ Φ }}.
+  (P ⊢ ▷ l1 ↦{q1} ?) →
+  (P ⊢ ▷ l2 ↦{q2} ?) →
+  (P ⊢ ▷ Φ (#(bool_decide (l1 = l2)))) →
+  P ⊢ WP #l1 = #l2 @ tid; E {{ Φ }}.
 Proof.
   iIntros (Hl1 Hl2 Hpost). iStartProof (iProp _).
   iIntros (?) "HP". rewrite wp_eq /wp_def. iIntros (𝓥 ->) "H𝓥 _".
diff --git a/gpfsl/logic/proofmode.v b/gpfsl/logic/proofmode.v
index c1461062b4748e19593563177078df5cf4aef30f..89ca558105bd392d77efc091a6db751df39d748f 100644
--- a/gpfsl/logic/proofmode.v
+++ b/gpfsl/logic/proofmode.v
@@ -133,7 +133,7 @@ Lemma tac_wp_alloc K Δ Δ' E j0 j1 j2 (n : Z) Φ tid :
   envs_entails Δ (WP fill K (Alloc #n) @ tid; E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal=> ??? HΔ. rewrite -wp_bind; [|done].
-  eapply wand_apply; first exact:wp_alloc.
+  eapply wand_apply; first by apply wand_entails, wp_alloc.
   rewrite -persistent_and_sep. apply and_intro; first by auto.
   rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l (Z.to_nat n)) as (Δ''&?&HΔ'); [rewrite Z2Nat.id //; lia|].