diff --git a/theories/examples/sc_stack.v b/theories/examples/sc_stack.v
index 198fca0305d5a0c29b6bb6814169be98efb7d8d0..3c8aa0ddee9dc7ba0449e7fedaf07ee1e8ede01e 100644
--- a/theories/examples/sc_stack.v
+++ b/theories/examples/sc_stack.v
@@ -10,6 +10,7 @@ Import uPred.
 
 Section SCStack.
 
+  Open Scope Z_scope.
   Local Notation next := 0.
   Local Notation data := 1.
 
@@ -42,166 +43,158 @@ Section SCStack.
   Section proof.
     Context `{fG : foundationG Σ}.
     Set Default Proof Using "Type".
-    Notation vPred := (@vPred Σ).
+    Notation vPred := (vProp Σ).
 
     Context (P: Z → vPred).
 
-    Local Open Scope VP.
-
-    Definition SCStack': (loc -c> list Z -c> @vPred_ofe Σ)
-                             -c> loc -c> list Z -c> @vPred_ofe Σ
+    Definition SCStack': (loc -c> list Z -c> vProp Σ)
+                             -c> loc -c> list Z -c> vProp Σ
     := (fun F l A =>
         ∃ l', ZplusPos next l ↦ l' ∗
         match A with
-        | nil => l' = 0
-        | v::A' => ■ (0 < l') ∗ Z.to_pos (l' + data) ↦ v ∗ P v
+        | nil => ⌜l' = 0⌝
+        | v::A' => ⌜0 < l'⌝ ∗ Z.to_pos (l' + data) ↦ v ∗ P v
                               ∗ ▷ F (Z.to_pos l') A'
-        end).
+        end)%I.
 
-    Close Scope VP.
-    Instance SCStack'_inhabited: Inhabited (loc -c> list Z -c> @vPred_ofe Σ)
-      := populate (λ _ _, True%VP).
+    Instance SCStack'_inhabited: Inhabited (loc -c> list Z -c> vProp Σ)
+      := populate (λ _ _, True)%I.
 
     Instance SCStack'_contractive:
         Contractive (SCStack').
     Proof.
-      intros ? ? ? H ? A ?.
-      repeat (apply uPred.exist_ne => ?).
-      apply uPred.sep_ne; [done|].
+      intros ? ? ? H ? A.
+      repeat (apply bi.exist_ne => ?).
+      apply bi.sep_ne; [done|].
       destruct A as [|v A]; [done|].
-      repeat (apply uPred.sep_ne; [done|]).
+      repeat (apply bi.sep_ne; [done|]).
       apply later_contractive. destruct n => //. by apply (H).
     Qed.
 
     Definition SCStack := fixpoint (SCStack').
 
     Lemma newStack_spec:
-      {{{{ True }}}}
+      {{{ ⎡PSCtx⎤ }}}
          newStack #()
-      {{{{ (s: loc), RET #s; SCStack s nil }}}}.
+      {{{ (s: loc), RET #s; SCStack s nil }}}.
     Proof.
-      intros. iViewUp. iIntros "#kI kS _ Post".
-      wp_seq. iNext. wp_bind Alloc.
-      iApply (alloc with "[%] kI kS []"); [done|done|done|].
-      iNext. iViewUp. iIntros (x) "kS os".
-      wp_seq. iNext.
+      iIntros (Φ) "#kI Post".
+      wp_seq. wp_bind Alloc.
+      wp_apply (alloc with "kI"); [done|].
+      iIntros (x) "os".
+      wp_seq.
       wp_bind ([_]_na <-_)%E.
-      iApply (na_write with "[%] kI kS [$os]"); [done|done|].
-      iNext. iViewUp; iIntros "kS os".
-      wp_seq. iNext. wp_value.
-      iApply ("Post" with "[%] kS [os]"); first done.
-      rewrite (fixpoint_unfold (SCStack') _ _ _ ).
+      wp_apply (na_write with "[$kI $os]"); [done|].
+      iIntros "os".
+      wp_seq.
+      iApply ("Post" with "[os]").
+      rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
       iExists _. by iFrame "os".
     Qed.
 
     Lemma push_spec s v A:
-      {{{{ SCStack s A ∗ P v }}}}
+      {{{ ⎡PSCtx⎤ ∗ SCStack s A ∗ P v }}}
          push #s #v
-      {{{{ RET #(); SCStack s (v :: A) }}}}.
+      {{{ RET #(); SCStack s (v :: A) }}}.
     Proof.
-      intros. iViewUp. iIntros "#kI kS (Stack & P) Post".
+      intros. iIntros "[#kI (Stack & P)] Post".
 
-      wp_lam. iNext. wp_value. wp_let. iNext.
+      wp_lam. wp_let.
       wp_bind (malloc _).
 
       iApply (wp_mask_mono); first auto.
-      iApply (malloc_spec with "[%] kI kS []"); [omega|done|done|].
-      iNext. iViewUp. iIntros (n) "kS oLs".
-      rewrite -bigop.vPred_big_opL_fold
-              big_op.big_sepL_cons big_op.big_opL_singleton.
-      iDestruct "oLs" as "(ol & od)".
-      wp_let. iNext. wp_bind ([_]_na <- _)%E. wp_op. iNext.
-      iApply (na_write with "[%] kI kS od"); [done|done|].
-      iNext. iViewUp. iIntros "kS od".
-      wp_seq. iNext. wp_bind ([_]_na)%E.
-
-      rewrite (fixpoint_unfold (SCStack') _ _ _ ).
+      wp_apply (malloc_spec with "kI []"); [omega|done|].
+      iIntros (n) "oLs".
+      iDestruct "oLs" as "(ol & od & _)".
+      wp_let. wp_bind ([_]_na <- _)%E. wp_op.
+      wp_apply (na_write with "[$kI $od]"); [done|].
+      iIntros "od".
+      wp_seq. wp_bind ([_]_na)%E.
+
+      rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
       iDestruct "Stack" as (h) "[oH oT]".
-      iApply (na_read with "[%] kI kS oH"); [done|done|].
-      iNext. iViewUp. iIntros (z) "kS [% oH]". subst z.
-      wp_seq. iNext. wp_bind ([_]_na <- _)%E. wp_op. iNext.
-      iApply (na_write with "[%] kI kS ol"); [done|done|].
-      iNext. iViewUp. iIntros "kS ol".
-      wp_seq. iNext. wp_op. iNext.
-      iApply (na_write with "[%] kI kS [$oH]"); [done|done|].
-
-      iNext. iViewUp. iIntros "kS oH".
-      iApply ("Post" with "[%] kS"); first done.
-
-      rewrite (fixpoint_unfold (SCStack') _ _ _ ).
+      wp_apply (na_read with "[$kI $oH]"); [done|].
+      iIntros (z) "[% oH]". subst z.
+      wp_seq. wp_bind ([_]_na <- _)%E. wp_op.
+      wp_apply (na_write with "[$kI $ol]"); [done|].
+      iIntros "ol".
+      wp_seq. wp_op.
+      wp_apply (na_write with "[$kI $oH]"); [done|].
+
+      iIntros "oH".
+      iApply ("Post").
+
+      rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
       iExists _. iFrame "oH P". iSplitL ""; first (iPureIntro; lia).
       iSplitL "od".
       - rewrite (_: Z.to_pos (Z.pos n + data) = ZplusPos data n); first done.
         rewrite /ZplusPos. f_equal. omega.
-      - iNext. rewrite (fixpoint_unfold (SCStack') _ _ _ ).
+      - iNext. rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
         iExists h. iFrame "oT ol".
     Qed.
 
     Lemma pop_spec s A:
-      {{{{ SCStack s A  }}}}
+      {{{ ⎡PSCtx⎤ ∗ SCStack s A  }}}
          pop #s
-      {{{{ (z: Z), RET #z;
+      {{{ (z: Z), RET #z;
            match A with
-           | nil => ■ (z = 0) ∗ SCStack s A
-           | v :: A' =>  ■ (z = v) ∗ SCStack s A' ∗ P v
-           end }}}}.
+           | nil => ⌜z = 0⌝ ∗ SCStack s A
+           | v :: A' =>  ⌜z = v⌝ ∗ SCStack s A' ∗ P v
+           end }}}.
     Proof.
-      intros. iViewUp. iIntros "#kI kS Stack Post".
-      wp_lam. iNext.
+      intros. iIntros "[#kI Stack] Post".
+      wp_lam.
       wp_bind ([_]_na)%E.
-      rewrite (fixpoint_unfold (SCStack') _ _ _ ).
+      rewrite {1}/SCStack (fixpoint_unfold (SCStack') _ _).
       iDestruct "Stack" as (h) "[oH oT]".
-      iApply (na_read with "[%] kI kS oH"); [done|done|].
-      iNext. iViewUp. iIntros (z) "kS [% oH]". subst z.
-      wp_seq. iNext.
+      wp_apply (na_read with "[$kI $oH]"); [done|].
+      iIntros (z) "[% oH]". subst z.
+      wp_seq.
       destruct A as [|v A'].
       - iDestruct "oT" as "%". subst h.
-        wp_op => [_|//]. iNext.
-        iApply wp_if_true. iNext.
-        wp_value.
-        iApply ("Post" with "[%] kS"); first done.
+        wp_op. wp_if.
+        iApply ("Post").
         iSplitL ""; first done.
-        rewrite (fixpoint_unfold (SCStack') _ _ _ ). iExists _. by iFrame "oH".
+        rewrite /SCStack (fixpoint_unfold (SCStack') _ _). iExists _. by iFrame "oH".
       - iDestruct "oT" as "(% & od & P & oT)".
-        wp_op => [?|_]; first omega. iNext.
-        iApply wp_if_false. iNext.
-        wp_bind ([_]_na)%E. wp_op. iNext. wp_op. iNext.
+        wp_op. case_bool_decide; first omega.
+        wp_if.
+        wp_bind ([_]_na)%E. wp_op. wp_op.
 
         rewrite (_: ZplusPos data (Z.to_pos h) = Z.to_pos (h + 1)); last first.
         { rewrite /ZplusPos. f_equal. rewrite Z2Pos.id; [omega|auto]. }
-        iApply (na_read with "[%] kI kS od"); [done|done|].
+        wp_apply (na_read with "[$kI $od]"); [done|].
 
-        iNext. iViewUp. iIntros (z) "kS [% od]". subst z.
-        wp_seq. iNext.
-        wp_bind ([_]_na)%E. wp_op. iNext. wp_op. iNext.
+        iIntros (z) "[% od]". subst z.
+        wp_seq.
+        wp_bind ([_]_na)%E. wp_op. wp_op.
 
-        rewrite (fixpoint_unfold (SCStack') _ _ _ ).
+        rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
         iDestruct "oT" as (h') "[oP oT]".
-        iApply (na_read with "[%] kI kS oP"); [done|done|].
-        iNext. iViewUp.  iIntros (z) "kS [% oP]". subst z.
-        wp_seq. iNext. wp_bind ([_]_na <- _)%E.
-        iApply (na_write with "[%] kI kS [$oH]"); [done|done|..].
-        iNext. iViewUp. iIntros "kS oH".
-        wp_seq. iNext.
-        wp_bind (Dealloc _). wp_op. iNext. wp_op. iNext.
+        wp_apply (na_read with "[$kI $oP]"); [done|].
+        iIntros (z) "[% oP]". subst z.
+        wp_seq. wp_bind ([_]_na <- _)%E.
+        wp_apply (na_write with "[$kI $oH]"); [done|].
+        iIntros "oH".
+        wp_seq.
+        wp_bind (Dealloc _). wp_op. wp_op.
 
         iApply (wp_mask_mono); first auto.
         rewrite (_: ZplusPos data (Z.to_pos h) = Z.to_pos (h + data)); last first.
         { rewrite /ZplusPos. f_equal. rewrite Z2Pos.id; [omega|auto]. }
-        iApply (dealloc with "[%] kI kS [$od]"); first done.
+        wp_apply (dealloc with "[$kI $od]").
 
-        iNext. iViewUp. iIntros "kS _".
-        wp_seq. iNext.
-        wp_bind (Dealloc _). wp_op. iNext. wp_op. iNext.
+        iIntros "_".
+        wp_seq.
+        wp_bind (Dealloc _). wp_op. wp_op.
         iApply (wp_mask_mono); first auto.
-        iApply (dealloc with "[%] kI kS [$oP]"); first done.
-        iNext. iViewUp. iIntros "kS _".
-        wp_seq. iNext.
+        wp_apply (dealloc with "[$kI $oP]").
+        iIntros "_".
+        wp_seq.
 
-        wp_value.
-        iApply ("Post" with "[%] kS"); first done.
+        iApply ("Post").
         iSplitL ""; first done. iFrame "P".
-        rewrite (fixpoint_unfold (SCStack') _ _ _ ).
+        rewrite /SCStack (fixpoint_unfold (SCStack') _ _).
         iExists _. by iFrame.
     Qed.
   End proof.