diff --git a/theories/effects/delim.v b/theories/effects/delim.v
index 1a862e5..638e05e 100644
--- a/theories/effects/delim.v
+++ b/theories/effects/delim.v
@@ -27,7 +27,25 @@ Program Definition resetE : opInterp :=
   |}.
 
 (* to apply the head of the meta continuation *)
-Program Definition popE : opInterp :=
+Program Definition pop_apply_E : opInterp :=
+  {|
+    Ins := (▶ ∙);
+    Outs := Empty_setO;
+  |}.
+
+Program Definition peek_apply_E : opInterp :=
+  {|
+    Ins := (▶ ∙);
+    Outs := Empty_setO;
+  |}.
+
+Program Definition pop_continue_E : opInterp :=
+  {|
+    Ins := (▶ ∙);
+    Outs := (▶ ∙);
+  |}.
+
+Program Definition pop_discard_E : opInterp :=
   {|
     Ins := (▶ ∙);
     Outs := Empty_setO;
@@ -40,12 +58,29 @@ Program Definition appContE : opInterp :=
     Outs := ▶ ∙;
   |} .
 
-Definition delimE := @[shiftE; resetE; popE;appContE].
+Program Definition shiftE' : opInterp :=
+  {|
+    Ins := ((▶ ∙ -n> ▶ ∙) -n> ▶ ∙);
+    Outs := (▶ ∙);
+  |}.
 
-Notation op_shift := (inl ()).
-Notation op_reset := (inr (inl ())).
-Notation op_pop := (inr (inr (inl ()))).
-Notation op_app_cont := (inr (inr (inr (inl ())))).
+Definition delimE := @[shiftE
+                       ; resetE
+                       ; pop_apply_E
+                       ; peek_apply_E
+                       ; pop_continue_E
+                       ; pop_discard_E
+                       ; appContE
+                       ; shiftE'].
+
+Notation op_shift        := (inl ()).
+Notation op_reset        := (inr (inl ())).
+Notation op_pop_apply    := (inr (inr (inl ()))).
+Notation op_peek_apply   := (inr (inr (inr (inl ())))).
+Notation op_pop_continue := (inr (inr (inr (inr (inl ()))))).
+Notation op_pop_discard  := (inr (inr (inr (inr (inr (inl ())))))).
+Notation op_app_cont     := (inr (inr (inr (inr (inr (inr (inl ()))))))).
+Notation op_shift'       := (inr (inr (inr (inr (inr (inr (inr (inl ())))))))).
 
 Section reifiers.
   Context {X} `{!Cofe X}.
@@ -71,20 +106,57 @@ Section reifiers.
         optionO (prodO (laterO X) state)).
   Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed.
 
+  Definition reify_pop_apply : (laterO X) * state * (Empty_setO -n> laterO X) →
+                               option (laterO X * state) :=
+    λ '(e, σ, _),
+      match σ with
+      | [] => Some (e, σ)
+      | k' :: σ' => Some (k' e, σ')
+      end.
+  #[export] Instance reify_pop_apply_ne :
+    NonExpansive (reify_pop_apply :
+        prodO (prodO (laterO X) state) (Empty_setO -n> laterO X) →
+        optionO (prodO (laterO X) state)).
+  Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed.
 
-  Definition reify_pop : (laterO X) * state * (Empty_setO -n> laterO X) →
+  Definition reify_peek_apply : (laterO X) * state * (Empty_setO -n> laterO X) →
                            option (laterO X * state) :=
     λ '(e, σ, _),
       match σ with
       | [] => Some (e, σ)
-      | k' :: σ' => Some (k' e, σ')
+      | k' :: σ' => Some (k' e, k' :: σ')
       end.
-  #[export] Instance reify_pop_ne :
-    NonExpansive (reify_pop :
+  #[export] Instance reify_peek_apply_ne :
+    NonExpansive (reify_peek_apply :
         prodO (prodO (laterO X) state) (Empty_setO -n> laterO X) →
         optionO (prodO (laterO X) state)).
   Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed.
 
+  Definition reify_pop_continue : (laterO X) * state * (laterO X -n> laterO X) →
+                                  option (laterO X * state) :=
+    λ '(e, σ, κ),
+      match σ with
+      | [] => Some (κ e, σ)
+      | _ :: σ' => Some (κ e, σ')
+      end.
+  #[export] Instance reify_pop_continue_ne :
+    NonExpansive (reify_pop_continue :
+        prodO (prodO (laterO X) state) (laterO X -n> laterO X) →
+        optionO (prodO (laterO X) state)).
+  Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed.
+
+  Definition reify_pop_discard : (laterO X) * state * (Empty_setO -n> laterO X) →
+                                 option (laterO X * state) :=
+    λ '(e, σ, _),
+      match σ with
+      | [] => Some (e, σ)
+      | _ :: σ' => Some (e, σ')
+      end.
+  #[export] Instance reify_pop_discard_ne :
+    NonExpansive (reify_pop_discard :
+        prodO (prodO (laterO X) state) (Empty_setO -n> laterO X) →
+        optionO (prodO (laterO X) state)).
+  Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed.
 
   Definition reify_app_cont : ((laterO X * (laterO (X -n> X))) * state * (laterO X -n> laterO X)) →
                               option (laterO X * state) :=
@@ -100,6 +172,17 @@ Section reifiers.
     repeat f_equiv; apply H.
   Qed.
 
+  Definition reify_shift' : ((laterO X -n> laterO X) -n> laterO X) *
+                              state * (laterO X -n> laterO X) →
+                            option (laterO X * state) :=
+    λ '(f, σ, k), Some ((f k): laterO X, tail (σ : state)).
+  #[export] Instance reify_shift_ne' :
+    NonExpansive (reify_shift' :
+      prodO (prodO ((laterO X -n> laterO X) -n> laterO X) state)
+        (laterO X -n> laterO X) →
+      optionO (prodO (laterO X) state)).
+  Proof. intros ?[[]][[]][[]]. simpl in *. repeat f_equiv; auto. Qed.
+
 End reifiers.
 
 Canonical Structure reify_delim : sReifier CtxDep.
@@ -109,11 +192,15 @@ Proof.
              sReifier_state := stateF
            |}.
   intros X HX op.
-  destruct op as [ | [ | [ | [| []]]]]; simpl.
+  destruct op as [ | [ | [ | [| [| [| [| [| []]]]]]]]]; simpl.
   - simple refine (OfeMor (reify_shift)).
   - simple refine (OfeMor (reify_reset)).
-  - simple refine (OfeMor (reify_pop)).
+  - simple refine (OfeMor (reify_pop_apply)).
+  - simple refine (OfeMor (reify_peek_apply)).
+  - simple refine (OfeMor (reify_pop_continue)).
+  - simple refine (OfeMor (reify_pop_discard)).
   - simple refine (OfeMor (reify_app_cont)).
+  - simple refine (OfeMor (reify_shift')).
 Defined.
 
 Section constructors.
@@ -126,13 +213,37 @@ Section constructors.
 
   (** ** POP *)
 
-  Program Definition POP : IT -n> IT :=
-    λne e, Vis (E:=E) (subEff_opid op_pop)
-             (subEff_ins (F:=delimE) (op:=op_pop) (Next e))
-             (Empty_setO_rec _ ◎ (subEff_outs (F:=delimE) (op:=op_pop))^-1).
+  Program Definition POP_APPLY : IT -n> IT :=
+    λne e, Vis (E:=E) (subEff_opid op_pop_apply)
+             (subEff_ins (F:=delimE) (op:=op_pop_apply) (Next e))
+             (Empty_setO_rec _ ◎ (subEff_outs (F:=delimE) (op:=op_pop_apply))^-1).
   Solve All Obligations with solve_proper.
 
-  Notation 𝒫 := (get_val POP).
+  Program Definition PEEK_APPLY : IT -n> IT :=
+    λne e, Vis (E:=E) (subEff_opid op_peek_apply)
+             (subEff_ins (F:=delimE) (op:=op_peek_apply) (Next e))
+             (Empty_setO_rec _ ◎ (subEff_outs (F:=delimE) (op:=op_peek_apply))^-1).
+  Solve All Obligations with solve_proper.
+
+  Program Definition POP_CONTINUE_ : (IT -n> IT) -n> IT -n> IT :=
+    λne k e, Vis (E:=E) (subEff_opid op_pop_continue)
+             (subEff_ins (F:=delimE) (op:=op_pop_continue) (Next e))
+             (laterO_map k ◎ (subEff_outs (F:=delimE) (op:=op_pop_continue))^-1).
+  Solve All Obligations with solve_proper.
+
+  Program Definition POP_CONTINUE : IT -n> IT :=
+    POP_CONTINUE_ idfun.
+
+  Program Definition POP_DISCARD : IT -n> IT :=
+    λne e, Vis (E:=E) (subEff_opid op_pop_discard)
+             (subEff_ins (F:=delimE) (op:=op_pop_discard) (Next e))
+             (Empty_setO_rec _ ◎ (subEff_outs (F:=delimE) (op:=op_pop_discard))^-1).
+  Solve All Obligations with solve_proper.
+
+  Notation 𝒫 := (get_val POP_APPLY).
+  Notation ℛ := (get_val PEEK_APPLY).
+  Notation 𝒞 := (get_val POP_CONTINUE).
+  Notation ℱ := (get_val POP_DISCARD).
 
   (** ** RESET *)
 
@@ -140,7 +251,7 @@ Section constructors.
                                 laterO IT -n>
                                 IT :=
     λne k e, Vis (E:=E) (subEff_opid op_reset)
-               (subEff_ins (F := delimE) (op := op_reset) (laterO_map 𝒫 e))
+               (subEff_ins (F := delimE) (op := op_reset) e)
                (k ◎ subEff_outs (F := delimE) (op := op_reset)^-1).
   Solve Obligations with solve_proper.
 
@@ -153,7 +264,7 @@ Section constructors.
                                 (laterO IT -n> laterO IT) -n>
                                 IT :=
     λne f k, Vis (E:=E) (subEff_opid op_shift)
-             (subEff_ins (F:=delimE) (op:=op_shift) ((laterO_map $ 𝒫) ◎ f))
+             (subEff_ins (F:=delimE) (op:=op_shift) f)
              (k ◎ (subEff_outs (F:=delimE) (op:=op_shift))^-1).
   Solve All Obligations with solve_proper.
 
@@ -186,7 +297,10 @@ Section constructors.
 
 End constructors.
 
-Notation 𝒫 := (get_val POP).
+Notation 𝒫 := (get_val POP_APPLY).
+Notation ℛ := (get_val PEEK_APPLY).
+Notation 𝒞 := (get_val POP_CONTINUE).
+Notation ℱ := (get_val POP_DISCARD).
 
 Section weakestpre.
   Context {sz : nat}.
@@ -208,7 +322,7 @@ Section weakestpre.
 
   Lemma wp_shift (σ : state) (f : (laterO IT -n> laterO IT) -n> laterO IT)
     (k : IT -n> IT) β {Hk : IT_hom k} Φ s :
-    laterO_map 𝒫 (f (laterO_map k)) ≡ Next β →
+    (f (laterO_map k)) ≡ Next β →
     has_substate σ -∗
     ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} β @ s {{ Φ }}) -∗
     WP@{rs} (k (SHIFT f)) @ s {{ Φ }}.
@@ -216,10 +330,15 @@ Section weakestpre.
     iIntros (Hp) "Hs Ha".
     unfold SHIFT. simpl.
     rewrite hom_vis.
-    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (laterO_map 𝒫 $ f (laterO_map k)) with "Hs").
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (f (laterO_map k)) with "Hs").
     {
-      simpl. do 2 f_equiv; last done. do 2 f_equiv.
-      rewrite ccompose_id_l. intro. simpl. by rewrite ofe_iso_21.
+      simpl. do 2 f_equiv; last done.
+      rewrite ccompose_id_l.
+      f_equiv.
+      intros ?.
+      simpl.
+      rewrite ofe_iso_21.
+      reflexivity.
     }
     { exact Hp. }
     iModIntro.
@@ -230,12 +349,12 @@ Section weakestpre.
     Φ s :
     has_substate σ -∗
     ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗
-       WP@{rs} 𝒫 e @ s {{ Φ }}) -∗
+       WP@{rs} e @ s {{ Φ }}) -∗
     WP@{rs} k $ (RESET (Next e)) @ s {{ Φ }}.
   Proof.
     iIntros "Hs Ha".
     unfold RESET. simpl. rewrite hom_vis.
-    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next $ 𝒫 e) with "Hs").
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next $ e) with "Hs").
     - simpl. repeat f_equiv. rewrite ccompose_id_l.
       trans ((laterO_map k) :: σ); last reflexivity.
       f_equiv. intro. simpl. by rewrite ofe_iso_21.
@@ -243,36 +362,168 @@ Section weakestpre.
     - iApply "Ha".
   Qed.
 
-  Lemma wp_pop_end (v : IT)
-    {HV : AsVal v}
+  Lemma wp_pop_apply_end (e : IT)
     Φ s :
-    has_substate [] -∗
-    ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} v @ s {{ Φ }}) -∗
-    WP@{rs} 𝒫 v @ s {{ Φ }}.
+    has_substate []
+    -∗ ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} e @ s {{ Φ }})
+    -∗ WP@{rs} POP_APPLY e @ s {{ Φ }}.
   Proof.
     iIntros "Hs Ha".
-    rewrite get_val_ITV. simpl.
-    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next v)) with "Hs").
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next e)) with "Hs").
     - simpl. reflexivity.
     - reflexivity.
     - done.
   Qed.
 
-  Lemma wp_pop_cons (σ : state) (v : IT) (k : IT -n> IT)
-    {HV : AsVal v}
+  Lemma wp_pop_apply_cons (σ : state) (e : IT) (k : IT -n> IT)
     Φ s :
-    has_substate ((laterO_map k) :: σ) -∗
-    ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k $ v @ s {{ Φ }}) -∗
-    WP@{rs} 𝒫 v @ s {{ Φ }}.
+    has_substate ((laterO_map k) :: σ)
+    -∗ ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k $ e @ s {{ Φ }})
+    -∗ WP@{rs} POP_APPLY e @ s {{ Φ }}.
   Proof.
     iIntros "Hs Ha".
-    rewrite get_val_ITV. simpl.
-    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((laterO_map k (Next v))) with "Hs").
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((laterO_map k (Next e))) with "Hs").
     - simpl. reflexivity.
     - reflexivity.
     - done.
   Qed.
 
+  Lemma wp_peek_apply_end (e : IT)
+    Φ s :
+    has_substate []
+    -∗ ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} e @ s {{ Φ }})
+    -∗ WP@{rs} PEEK_APPLY e @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next e)) with "Hs").
+    - simpl. reflexivity.
+    - reflexivity.
+    - done.
+  Qed.
+
+  Lemma wp_peek_apply_cons (σ : state) (e : IT) (k : IT -n> IT)
+    Φ s :
+    has_substate ((laterO_map k) :: σ)
+    -∗ ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ WP@{rs} k $ e @ s {{ Φ }})
+    -∗ WP@{rs} PEEK_APPLY e @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((laterO_map k (Next e))) with "Hs").
+    - simpl. reflexivity.
+    - reflexivity.
+    - done.
+  Qed.
+
+  Lemma wp_pop_continue (e : IT) σ
+    Φ s :
+    has_substate σ
+    -∗ ▷ (£ 1 -∗ has_substate (tail σ) -∗ WP@{rs} e @ s {{ Φ }})
+    -∗ WP@{rs} POP_CONTINUE e @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    destruct σ.
+    - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next e)) with "Hs").
+      + simpl; rewrite ofe_iso_21 later_map_Next; reflexivity.
+      + reflexivity.
+      + done.
+    - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next e)) with "Hs").
+      + simpl; rewrite ofe_iso_21 later_map_Next; reflexivity.
+      + reflexivity.
+      + done.
+  Qed.
+
+  Lemma wp_pop_discard (e : IT) σ
+    Φ s :
+    has_substate σ
+    -∗ ▷ (£ 1 -∗ has_substate (tail σ) -∗ WP@{rs} e @ s {{ Φ }})
+    -∗ WP@{rs} POP_DISCARD e @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    destruct σ.
+    - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next e)) with "Hs").
+      + simpl.
+        reflexivity.
+      + reflexivity.
+      + done.
+    - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next e)) with "Hs").
+      + simpl.
+        reflexivity.
+      + reflexivity.
+      + done.
+  Qed.
+
+  Lemma wp_pop_apply_end' (v : IT)
+    {HV : AsVal v}
+    Φ s :
+    has_substate []
+    -∗ ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} v @ s {{ Φ }})
+    -∗ WP@{rs} 𝒫 v @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    rewrite get_val_ITV. simpl.
+    iApply (wp_pop_apply_end with "Hs Ha").
+  Qed.
+
+  Lemma wp_pop_apply_cons' (σ : state) (v : IT) (k : IT -n> IT)
+    {HV : AsVal v}
+    Φ s :
+    has_substate ((laterO_map k) :: σ)
+    -∗ ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k $ v @ s {{ Φ }})
+    -∗ WP@{rs} 𝒫 v @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    rewrite get_val_ITV. simpl.
+    iApply (wp_pop_apply_cons with "Hs Ha").
+  Qed.
+
+  Lemma wp_peek_apply_end' (v : IT)
+    {HV : AsVal v}
+    Φ s :
+    has_substate []
+    -∗ ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} v @ s {{ Φ }})
+    -∗ WP@{rs} ℛ v @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    rewrite get_val_ITV. simpl.
+    iApply (wp_peek_apply_end with "Hs Ha").
+  Qed.
+
+  Lemma wp_peek_apply_cons' (σ : state) (v : IT) (k : IT -n> IT)
+    {HV : AsVal v}
+    Φ s :
+    has_substate ((laterO_map k) :: σ)
+    -∗ ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ WP@{rs} k $ v @ s {{ Φ }})
+    -∗ WP@{rs} ℛ v @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    rewrite get_val_ITV. simpl.
+    iApply (wp_peek_apply_cons with "Hs Ha").
+  Qed.
+
+  Lemma wp_pop_continue' (v : IT) σ
+    {HV : AsVal v}
+    Φ s :
+    has_substate σ
+    -∗ ▷ (£ 1 -∗ has_substate (tail σ) -∗ WP@{rs} v @ s {{ Φ }})
+    -∗ WP@{rs} 𝒞 v @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    rewrite get_val_ITV. simpl.
+    iApply (wp_pop_continue with "Hs Ha").
+  Qed.
+
+  Lemma wp_pop_discard' (v : IT) σ
+    {HV : AsVal v}
+    Φ s :
+    has_substate σ
+    -∗ ▷ (£ 1 -∗ has_substate (tail σ) -∗ WP@{rs} v @ s {{ Φ }})
+    -∗ WP@{rs} ℱ v @ s {{ Φ }}.
+  Proof.
+    iIntros "Hs Ha".
+    rewrite get_val_ITV. simpl.
+    iApply (wp_pop_discard with "Hs Ha").
+  Qed.
+
   Lemma wp_app_cont (σ : state) (e : laterO IT) (k' : laterO (IT -n> IT))
     (k : IT -n> IT) β {Hk : IT_hom k}
     Φ s :
diff --git a/theories/examples/delim_lang/adeq.v b/theories/examples/delim_lang/adeq.v
index 42a61b4..ef5eac5 100644
--- a/theories/examples/delim_lang/adeq.v
+++ b/theories/examples/delim_lang/adeq.v
@@ -138,7 +138,7 @@ Section logrel.
 
   Lemma wp_shift (σ : stateF ♯ IT) (f : (laterO IT -n> laterO IT) -n> laterO IT)
     (k : IT -n> IT) β {Hk : IT_hom k} Φ :
-    laterO_map 𝒫 (f (laterO_map k)) ≡ Next β →
+    (f (laterO_map k)) ≡ Next β →
     has_cont_stack σ -∗
     ▷ (£ 1 -∗ has_cont_stack σ -∗ WP β {{ Φ }}) -∗
     WP (k (SHIFT f)) {{ Φ }}.
@@ -155,7 +155,7 @@ Section logrel.
     Φ :
     has_cont_stack σ -∗
     ▷ (£ 1 -∗ has_cont_stack ((laterO_map k) :: σ) -∗
-       WP 𝒫 e {{ Φ }}) -∗
+       WP e {{ Φ }}) -∗
     WP k $ (RESET (Next e)) {{ Φ }}.
   Proof.
     iIntros "(Hs & G) Ha".
@@ -169,7 +169,7 @@ Section logrel.
     now subst F.
   Qed.
 
-  Lemma wp_pop_end (v : IT)
+  Lemma wp_pop_apply_end (v : IT)
     {HV : AsVal v}
     Φ :
     has_cont_stack [] -∗
@@ -177,14 +177,14 @@ Section logrel.
     WP 𝒫 v {{ Φ }}.
   Proof.
     iIntros "(Hs & G) Ha".
-    iApply (wp_pop_end with "Hs").
+    iApply (wp_pop_apply_end' with "Hs").
     iNext.
     iIntros "HCr Hs".
     iApply ("Ha" with "HCr").
     now iFrame.
   Qed.
 
-  Lemma wp_pop_cons (σ : stateF ♯ IT) (v : IT) (k : IT -n> IT)
+  Lemma wp_pop_apply_cons (σ : stateF ♯ IT) (v : IT) (k : IT -n> IT)
     {HV : AsVal v}
     Φ :
     has_cont_stack ((laterO_map k) :: σ) -∗
@@ -192,7 +192,7 @@ Section logrel.
     WP 𝒫 v {{ Φ }}.
   Proof.
     iIntros "(Hs & (_ & G)) Ha".
-    iApply (wp_pop_cons with "Hs").
+    iApply (wp_pop_apply_cons' with "Hs").
     iNext.
     iIntros "HCr Hs".
     iApply ("Ha" with "HCr").
@@ -227,7 +227,7 @@ Section logrel.
   Definition logrel_ectx (V W : ITV -n> iProp) (κ : HOM) : iProp :=
     (□ ∀ (βv : ITV) σ,
        has_cont_stack σ
-       -∗ V βv -∗ WP (`κ (IT_of_V βv)) {{ βv, W βv ∗ has_cont_stack σ }})%I.
+       -∗ V βv -∗ WP (`κ (IT_of_V βv)) {{ βv, W βv }})%I.
   Local Instance logrel_ectx_ne :
     ∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) logrel_ectx.
   Proof. solve_proper. Qed.
@@ -238,7 +238,7 @@ Section logrel.
       (∀ (κ : HOM) (σ : stateF ♯ IT),
          logrel_ectx τ α κ
          -∗ has_cont_stack σ
-         -∗ WP (`κ βe) {{ βv, β βv ∗ has_cont_stack σ }})%I.
+         -∗ WP (`κ βe) {{ βv, β βv }})%I.
   Next Obligation. solve_proper. Qed.
   Local Instance logrel_expr_ne
     : (∀ n, Proper (dist n
@@ -300,59 +300,495 @@ Section logrel.
   Program Definition 𝒫_HOM : @HOM sz CtxDep R _ _ := exist _ 𝒫 _.
   Next Obligation. apply _. Qed.
 
-  Lemma 𝒫_logrel_cont τ : ⊢ logrel_ectx (interp_ty τ) (interp_ty τ) 𝒫_HOM.
+  Lemma HOM_id_logrel_ectx τ : ⊢ logrel_ectx (interp_ty τ) (interp_ty τ) HOM_id.
   Proof.
-    iLöb as "IH".
     iModIntro.
     iIntros (αv σ) "G #H".
-    destruct σ as [| ? σ].
-    - iApply (wp_pop_end with "G").
-      iNext.
-      iIntros "_ G".
-      iApply wp_val.
-      iModIntro.
-      by iFrame "H".
-      (* by iExists []. *)
-    - admit.
+    by iApply wp_val.
+  Qed.
+
+  Inductive head_step {S} : expr S → expr S → nat * nat → Prop :=
+  (* this rule is a bit unneccessary,
+     filling ctx with stuff is taken care of in the last rule *)
+  | BetaEContS k v :
+    head_step
+      (AppCont (Val $ ContV k) (Val v))
+      (fill k (Val v))
+      (1, 1)
+  | ResetPureS v :
+    head_step
+      (Reset (Val v))
+      (Val v)
+      (2, 1)
+  | ResetEffS e (E : cont S) :
+    head_step
+      (Reset (fill E (Shift e)))
+      (Reset (subst (F := expr) (Inc := inc) e
+                (Val (RecV (Reset
+                              (fill (shift (Inc := inc) (shift (Inc := inc) E))
+                                 (Var VZ)))))))
+      (3, 1)
+  .
+
+  Program Definition shift_interp_new {S : Set} (env : @interp_scope F R _ S)
+    (e : @interp_scope F R _ (inc S) -n> IT) :=
+    SHIFT (laterO_map 𝒫 ◎ (λne (k : laterO IT -n> laterO IT),
+               (Next (e (extend_scope env (λit x, Tau (k (Next x)))))))).
+  Next Obligation. solve_proper. Defined.
+  Next Obligation.
+    solve_proper_prepare.
+    do 2 f_equiv.
+    intros [| ?]; simpl.
+    - do 2 f_equiv.
+      intros ?; simpl.
+      f_equiv.
+      done.
+    - reflexivity.
+  Qed.
+
+  Program Definition reset_interp_new {S} (e : S -n> IT) : S -n> IT :=
+    λne env, RESET (laterO_map 𝒫 (Next $ e env)).
+  Solve All Obligations with solve_proper.
+
+  Opaque interp_cont.
+  (* continuation stack modification can be changed *)
+  Lemma soundness_head_step_sanity_check1 {S : Set} (env : interp_scope S) K E
+    (e : expr S)
+    (σ : stateF ♯ IT) (σr : gState_rest sR_idx rs ♯ IT) :
+    reify (gReifiers_sReifier rs)
+      ((interp_cont _ K) env
+         (* can be as well *)
+         (* (reset_interp_new (interp_expr rs e) env) *)
+         (RESET (later_map E (Next (interp_expr rs e env))))
+      )
+      ((gState_decomp' sR_idx ^-1) (sR_state σ, σr))
+      ≡ ((gState_decomp' sR_idx ^-1)
+           (sR_state (laterO_map ((interp_cont _ K) env) :: σ), σr)
+        , Tick (E (interp_expr rs e env))).
+  Proof.
+    Opaque POP_CONTINUE.
+    set (Ksem := interp_cont rs K env).
+    set (Vsem := interp_expr rs e env).
+    simpl.
+    rewrite later_map_Next.
+    unfold RESET.
+    trans (reify (gReifiers_sReifier rs)
+             ((RESET_ (laterO_map Ksem)
+                 (Next (E Vsem))))
+             ((gState_decomp' sR_idx ^-1) (sR_state σ, σr))).
+    { f_equiv; last done.
+      f_equiv.
+      rewrite hom_vis.
+      Transparent RESET_.
+      simpl.
+      do 2 f_equiv; first solve_proper.
+      by rewrite ccompose_id_l.
+    }
+    rewrite reify_vis_eq_ctx_dep//; last first.
+    {
+      epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_reset)
+                     (Next (E Vsem))
+                     (Next (E Vsem))
+                     (laterO_map Ksem)
+                     σ (laterO_map Ksem :: σ) σr) as Hr.
+      simpl in Hr|-*.
+      erewrite <-Hr; last done.
+      repeat f_equiv; last done.
+      solve_proper.
+    }
+    f_equiv.
+    rewrite <-Tick_eq.
+    reflexivity.
+  Qed.
+
+  Lemma soundness_head_step_sanity_check2 {S : Set} (env : interp_scope S) K
+    (e : expr (inc S))
+    (σ : stateF ♯ IT) (σr : gState_rest sR_idx rs ♯ IT) :
+    reify (gReifiers_sReifier rs)
+      ((interp_cont _ K) env
+         (shift_interp_new env (interp_expr _ e)))
+      ((gState_decomp' sR_idx ^-1) (sR_state σ, σr))
+      ≡ ((gState_decomp' sR_idx ^-1)
+           (sR_state σ, σr)
+        , Tick (𝒫 ((interp_expr _ e)
+                  (extend_scope env
+                     (λit x : IT, Tau (later_map (interp_cont rs K env) (Next x))))))).
+  Proof.
+    Opaque extend_scope.
+    set (Ksem := interp_cont rs K env).
+    set (Esem := interp_expr rs e).
+    simpl.
+    unfold shift_interp_new.
+    unfold SHIFT.
+    cbn [ofe_mor_car].
+    set (b := OfeMor _).
+    trans (reify (gReifiers_sReifier rs)
+             (SHIFT_ (laterO_map 𝒫 ◎ b) (laterO_map Ksem))
+             ((gState_decomp' sR_idx ^-1) (sR_state σ, σr))).
+    { subst b.
+      f_equiv; last done.
+      f_equiv.
+      rewrite hom_vis.
+      Transparent SHIFT_.
+      simpl.
+      do 2 f_equiv; first solve_proper.
+      by rewrite ccompose_id_l.
+    }
+
+    rewrite reify_vis_eq_ctx_dep//; last first.
+    {
+      epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_shift)
+                     (laterO_map 𝒫 ◎ b)
+                     ((laterO_map 𝒫 ◎ b) (laterO_map Ksem))
+                     (laterO_map Ksem)
+                     σ σ σr) as Hr.
+      simpl in Hr|-*.
+      erewrite <-Hr; last done.
+      repeat f_equiv; last done.
+      solve_proper.
+    }
+    f_equiv.
+    rewrite <-Tick_eq.
+    simpl.
+    reflexivity.
+  Qed.
+
+  Lemma soundness_head_step_sanity_check3 {S : Set} (env : @interp_scope F R _ S)
+    (K : IT -n> IT)
+    (e : expr S)
+    (σ : stateF ♯ IT) (σr : gState_rest sR_idx rs ♯ IT) :
+    reify (gReifiers_sReifier rs) (PEEK_APPLY (interp_expr _ e env))
+      ((gState_decomp' sR_idx ^-1) (sR_state (laterO_map K :: σ), σr))
+      ≡ (gState_recomp σr (sR_state (laterO_map K :: σ)), Tick (K (interp_expr _ e env))).
+  Proof.
+    set (Esem := interp_expr rs e env).
+    rewrite reify_vis_eq_ctx_dep//; last first.
+    {
+      epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_peek_apply)
+                     (Next Esem)
+                     (Next (K Esem))
+                     (Empty_setO_rec _)
+                     (laterO_map K :: σ) (laterO_map K :: σ) σr) as Hr.
+      simpl in Hr|-*.
+      erewrite <-Hr; first last.
+      - rewrite later_map_Next.
+        reflexivity.
+      - repeat f_equiv.
+        solve_proper.
+    }
+    f_equiv.
+    rewrite <-Tick_eq.
+    reflexivity.
+  Qed.
+
+  Lemma soundness_head_step_sanity_check4 {S : Set} (env : @interp_scope F R _ S)
+    (K : IT -n> IT)
+    (e : expr S)
+    (σ : stateF ♯ IT) (σr : gState_rest sR_idx rs ♯ IT) :
+    reify (gReifiers_sReifier rs) (POP_APPLY (interp_expr _ e env))
+      ((gState_decomp' sR_idx ^-1) (sR_state (laterO_map K :: σ), σr))
+      ≡ (gState_recomp σr (sR_state σ), Tick (K (interp_expr _ e env))).
+  Proof.
+    set (Esem := interp_expr rs e env).
+    rewrite reify_vis_eq_ctx_dep//; last first.
+    {
+      epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_pop_apply)
+                     (Next Esem)
+                     (Next (K Esem))
+                     (Empty_setO_rec _)
+                     (laterO_map K :: σ) σ σr) as Hr.
+      simpl in Hr|-*.
+      erewrite <-Hr; first last.
+      - rewrite later_map_Next.
+        reflexivity.
+      - repeat f_equiv.
+        solve_proper.
+    }
+    f_equiv.
+    rewrite <-Tick_eq.
+    reflexivity.
+  Qed.
+
+  (* note that here, strictly speaking, we simplify things a bit:
+     in the full calculus there should be two rules
+     1. Ectx_step for "dirty" contexts and classical lambda terms
+     2. Ectx_step for combination of "dirty" context, reset and "pure" context
+        for reset-shift rule
+   *)
+  Inductive prim_step {S} (e1 : expr S)  (e2 : expr S) (n : nat * nat) : Prop:=
+    Ectx_step (K : cont S) e1' e2' :
+      e1 = fill K e1' → e2 = fill K e2' →
+      head_step e1' e2' n → prim_step e1 e2 n.
+
+  Inductive prim_steps {S} : expr S → expr S → nat * nat → Prop :=
+  | prim_steps_zero e :
+    prim_steps e e (0, 0)
+  | prim_steps_abit e1 e2 e3 n1 m1 n2 m2 :
+    prim_step e1 e2 (n1, m1) →
+    prim_steps e2 e3 (n2, m2) →
+    prim_steps e1 e3 (n1 + n2, m1 + m2)%nat
+  .
+
+  Notation "'⟦' e '⟧' γ" := (interp_expr rs e γ) (at level 50, only printing).
+  Notation "'⟦' v '⟧' γ" := (interp_val rs v γ) (at level 50, only printing).
+  Notation "'⟦' K '⟧' γ" := (interp_cont rs K γ) (at level 50, only printing).
+  Notation "e '⟶' e' '/' n" := (prim_step e e' n) (at level 50, only printing).
+  Notation "e '⟶*' e' '/' n" := (prim_steps e e' n) (at level 50, only printing).
+  Notation "e '→' e' '/' n" := (head_step e e' n) (at level 50, only printing).
+
+  Lemma soundness {S} (e1 e2 : expr S) σ (σr : gState_rest sR_idx rs ♯ IT) n m
+    (env : interp_scope S) :
+    prim_step e1 e2 (n, m) →
+    ∃ σ', ssteps (gReifiers_sReifier rs)
+            (interp_expr _ e1 env) (gState_recomp σr (sR_state σ))
+            (interp_expr _ e2 env) (gState_recomp σr (sR_state σ')) n.
+  Proof.
+    Opaque gState_decomp gState_recomp.
+    inversion 1; simplify_eq/=.
+    inversion H2; subst; simpl.
+    - exists σ.
+      change 1 with (Nat.add 1 0). econstructor; last first.
+      { apply ssteps_zero; reflexivity. }
+      eapply sstep_reify.
+      {
+        rewrite interp_comp. simpl.
+        fold (@interp_val sz rs _ R _ _ _ v).
+        rewrite get_val_ITV.
+        simpl.
+        rewrite get_fun_fun.
+        simpl.
+        rewrite hom_vis.
+        reflexivity.
+      }
+      (* skip *)
+      admit.
+    - exists σ.
+      change 2 with (Nat.add 1 1). econstructor.
+      + eapply sstep_reify.
+        {
+          rewrite interp_comp. simpl.
+          fold (@interp_val sz rs _ R _ _ _ v).
+          rewrite hom_vis.
+          reflexivity.
+        }
+        assert ((interp_expr rs (K ⟪ reset v ⟫) env)
+                = ((interp_cont _ K) env
+                     (reset_interp_new (interp_expr rs v) env)
+                     (* (RESET (later_map ℛ *)
+                     (*           (Next (interp_expr rs v env)))) *))) as ->.
+        {
+          (* fill + different reset *)
+          admit.
+        }
+        rewrite soundness_head_step_sanity_check1.
+        reflexivity.
+      + change 1 with (Nat.add 1 0). econstructor; last first.
+        { apply ssteps_zero; reflexivity. }
+        eapply sstep_reify.
+        {
+          Transparent POP_APPLY.
+          unfold POP_APPLY.
+          rewrite get_val_ITV.
+          cbn [ofe_mor_car].
+          reflexivity.
+        }
+        assert ((interp_expr rs v env)
+                = (interp_val rs v env)) as ->.
+        { reflexivity. }
+        pose proof (@get_val_ITV _ _ _ (interp_val _ v env) _ POP_APPLY).
+        epose proof (soundness_head_step_sanity_check4 env (interp_cont _ K env) v σ σr).
+        (* peek_apply + get val *)
+        admit.
+    - exists σ.
+      change 3 with (Nat.add 1 2). econstructor.
+      + eapply sstep_reify.
+        {
+          rewrite interp_comp. simpl.
+          fold (@interp_expr sz rs _ R _ _ _ (E ⟪ shift/cc e ⟫)).
+          rewrite hom_vis.
+          reflexivity.
+        }
+        assert ((interp_expr rs (K ⟪ reset (E ⟪ shift/cc e ⟫) ⟫) env)
+                = ((interp_cont _ K) env
+               (reset_interp_new (interp_expr rs (E ⟪ shift/cc e ⟫)) env)
+                     (* (RESET (later_map ℛ *)
+                     (*           (Next (interp_expr rs (E ⟪ shift/cc e ⟫) env)))) *))) as ->.
+        {
+          (* fill + different reset *)
+          admit.
+        }
+        rewrite soundness_head_step_sanity_check1.
+        reflexivity.
+      + change 2 with (Nat.add 1 1). econstructor.
+        * rewrite interp_comp.
+          assert (interp_expr _ (shift/cc e) env = shift_interp_new env (interp_expr _ e)) as ->.
+          {
+            (* different shift *)
+            admit.
+          }
+          unfold shift_interp_new.
+          unfold SHIFT.
+          cbn [ofe_mor_car].
+          set (b := OfeMor _).
+          assert ((𝒫 ((interp_cont _ E env) (SHIFT_ (laterO_map 𝒫 ◎ b) idfun)))
+                    ≡ (𝒫 (SHIFT_ (laterO_map 𝒫 ◎ b) (laterO_map (interp_cont _ E env))))) as ->.
+          { subst b.
+            f_equiv.
+            rewrite hom_vis.
+            Transparent SHIFT_.
+            simpl.
+            do 2 f_equiv; first solve_proper.
+            by rewrite ccompose_id_l.
+          }
+          assert ((𝒫 (SHIFT_ (laterO_map 𝒫 ◎ b) (laterO_map (interp_cont _ E env))))
+                    ≡ (SHIFT_ (laterO_map 𝒫 ◎ b) (laterO_map (𝒫 ◎ (interp_cont _ E env))))) as ->.
+          {
+            rewrite get_val_vis.
+            unfold SHIFT_.
+            simpl.
+            f_equiv.
+            intros ?; simpl.
+            rewrite later_map_compose.
+            reflexivity.
+          }
+          eapply sstep_reify.
+          {
+            unfold SHIFT_.
+            cbn [ofe_mor_car].
+            reflexivity.
+          }
+          rewrite reify_vis_eq_ctx_dep//; last first.
+          {
+            epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_shift)
+                           (laterO_map 𝒫 ◎ b)
+                           ((laterO_map 𝒫 ◎ b) (laterO_map (𝒫 ◎ (interp_cont _ E env))))
+                           (laterO_map (𝒫 ◎ (interp_cont _ E env)))
+                           (laterO_map (interp_cont _ K env) :: σ)
+                           (laterO_map (interp_cont _ K env) :: σ) σr) as Hr.
+            simpl in Hr|-*.
+            erewrite <-Hr; last done.
+            repeat f_equiv; last done.
+            - solve_proper_prepare.
+              destruct x, y.
+              simpl.
+              f_equiv.
+              + apply H0.
+              + f_equiv; last apply H0.
+                reflexivity.
+            - reflexivity.
+          }
+          f_equiv.
+          -- reflexivity.
+          -- rewrite <-Tick_eq.
+             reflexivity.
+        * Opaque SHIFT_.
+          Opaque RESET_.
+          Opaque extend_scope.
+          change 1 with (Nat.add 1 0). econstructor; last first.
+          { apply ssteps_zero; reflexivity. }
+
+          simpl (ofe_mor_car _ _ idfun).
+          cbn [ofe_mor_car].
+
+          (* rewrite interp_comp. *)
+          set (c := subst _ _).
+          rewrite later_map_Next.
+          cbn [later_car].
+
+          assert ((interp_expr rs (K ⟪ reset c ⟫) env)
+                  = ((interp_cont _ K) env
+                 (reset_interp_new (interp_expr rs c) env)
+                       (* (RESET (later_map ℛ *)
+                       (*           (Next (interp_expr rs c env)))) *))) as ->.
+          {
+            (* fill + different reset *)
+            admit.
+          }
+          unfold reset_interp_new.
+          cbn [ofe_mor_car].
+          unfold RESET.
+
+          (* subst c.
+             term_simpl.
+             rewrite interp_expr_subst.
+           *)
+
+          (*
+             missing reset outside
+             missing reset inside
+             -ctrl-
+             instead of
+             +ctrl+
+             (1st represents delimiter outside, 2nd represents delimiter inside
+           *)
+
+        admit.
   Admitted.
 
+  Program Definition interp_reset {S} (e : S -n> IT) : S -n> IT :=
+    λne env, RESET (laterO_map 𝒫 (Next $ e env)).
+  Solve All Obligations with solve_proper.
+
+  Program Definition interp_shift {S} (e : @interp_scope F R _ (inc S) -n> IT) :
+    interp_scope S -n> IT :=
+    λne env, SHIFT (laterO_map 𝒫 ◎ (λne (k : laterO IT -n> laterO IT),
+                        (Next (e (extend_scope env (λit x, Tau (k (Next x)))))))).
+  Solve All Obligations with try solve_proper.
+  Next Obligation.
+    solve_proper_prepare.
+    repeat f_equiv.
+    intros ?; simpl.
+    f_equiv.
+    apply H.
+  Qed.
+  Next Obligation.
+    solve_proper_prepare.
+    do 3 f_equiv.
+    intros ?; simpl.
+    do 2 f_equiv.
+    intros [| ?]; simpl.
+    - solve_proper.
+    - solve_proper.
+  Qed.
+
+  Local Instance aaaaaa {S : Set} (e : @interp_scope F R _ S -n> IT) :
+    NonExpansive ((λ env, RESET (laterO_map 𝒫 (Next $ e env)))).
+  Proof. solve_proper. Qed.
+
   Lemma compat_reset {S : Set} (Γ : S -> ty) e τ' τ A :
-        ⊢ valid Γ e τ' τ' τ -∗ valid Γ (interp_reset rs e) τ A A.
+    ⊢ valid Γ e τ' τ' τ
+      -∗ valid Γ (λne env, RESET (laterO_map 𝒫 (Next $ e env))) τ A A.
   Proof.
     iIntros "#H".
     iModIntro.
     iIntros (γ) "#Henv".
     iIntros (κ σ) "#Hκ Hσ".
     iApply (wp_reset with "Hσ").
+    simpl.
     iNext.
     iIntros "_ Hσ".
+    (* iApply (delim.wp_pop_apply_cons with "[Hσ] "). *)
+    (* - admit. *)
+    (* -  *)
     iSpecialize ("H" $! γ with "Henv").
-    iSpecialize ("H" $! HOM_id (laterO_map (`κ) :: σ) with "[] Hσ").
-    - iModIntro.
-      iIntros (βv σ') "Hσ' #H".
-      iApply wp_val.
-      iModIntro.
-      by iFrame "H".
-      (* by iExists σ'. *)
-    - simpl.
-      admit.
   Admitted.
 
+  (* breaks here, reset is still morally correct, as it is just a delimiter *)
   Lemma compat_shift {S : Set} (Γ : S -> ty) e τ' α τ β :
     ⊢ valid (Γ ▹ (Tcont τ α)) e τ' τ' β
-      -∗ valid Γ (interp_shift _ e) τ α β.
+      -∗ valid Γ (interp_shift e) τ α β.
   Proof.
     iIntros "#H".
     iModIntro.
     iIntros (γ) "#Henv".
     iIntros (κ σ) "#Hκ Hσ".
-    assert (interp_shift rs e γ ≡ idfun $ interp_shift rs e γ) as ->.
-    { reflexivity. }
+    (* assert (interp_shift e γ ≡ idfun $ interp_shift e γ) as ->. *)
+    (* { reflexivity. } *)
     iApply (wp_shift with "Hσ").
     { apply (laterO_map_Next 𝒫). }
     {
       iNext.
-      iIntros "HCr Hσ'".
+      iIntros "_ Hσ'".
       set (F := Next _).
       set (γ' := extend_scope γ _).
       iSpecialize ("H" $! γ' with "[Hκ]").
@@ -362,7 +798,7 @@ Section logrel.
           iIntros (Pα σ') "#Hκ' Hσ".
           iApply ("Hκ'" $! (FunV F) σ' with "Hσ").
           iExists κ.
-          iSplit; first (iPureIntro; reflexivity).
+          iSplit; first (* (iPureIntro; reflexivity). *) admit.
           iModIntro.
           iModIntro.
           iIntros (βv σ'') "Hσ'' #HHH".
@@ -370,12 +806,12 @@ Section logrel.
         + iIntros (a).
           iModIntro.
           iApply "Henv".
-      - iSpecialize ("H" $! 𝒫_HOM σ).
-        iSpecialize ("H" with "[] Hσ'").
-        + iApply 𝒫_logrel_cont.
-        + iApply "H".
+      - iSpecialize ("H" $! HOM_id σ with "[] Hσ'").
+        + iApply HOM_id_logrel_ectx.
+        + simpl.
+          admit.
     }
-  Qed.
+  Admitted.
 
   Lemma compat_var {S : Set} (Γ : S -> ty) (x : S) α :
     ⊢ valid Γ (interp_var x) (Γ x) α α.
@@ -394,10 +830,9 @@ Section logrel.
     iApply (wp_wand with "[Hκ Hσ]").
     - iApply ("Hκ" $! (RetV n) σ with "Hσ").
       iExists _; by iPureIntro.
-    - iIntros (v) "(#H & G)".
+    - iIntros (v) "#H".
       iModIntro.
       iFrame "H".
-      iFrame "G".
   Qed.
 
   Lemma logrel_of_val τ v α :
@@ -407,10 +842,9 @@ Section logrel.
     iIntros (κ σ) "#Hκ Hσ".
     iApply (wp_wand with "[Hκ Hσ]").
     - by iApply ("Hκ" $! v σ with "Hσ").
-    - iIntros (w) "(#G & F)".
+    - iIntros (w) "#G".
       iModIntro.
       iFrame "G".
-      iFrame "F".
   Qed.
 
   Lemma compat_recV {S : Set} (Γ : S -> ty)
@@ -593,9 +1027,8 @@ Section logrel.
       rewrite <- Tick_eq.
       iApply wp_tick.
       iNext.
-      (* iApply ("Hv" $! w (laterO_map (`κ) :: σ''') with "Hσ Hw"). *)
-      admit.
-  Admitted.
+      iApply ("Hv" $! w (laterO_map (`κ) :: σ''') with "Hσ Hw").
+  Qed.
 
   Program Definition NatOpRSCtx_HOM {S : Set} (op : nat_op)
     (α : @interp_scope F R _ S -n> IT) (env : @interp_scope F R _ S)
@@ -658,7 +1091,6 @@ Section logrel.
 
     iDestruct "Hw" as "(%n & #HEQ1)".
     iDestruct "Hv" as "(%n' & #HEQ2)".
-
     (* iApply ("Hκ" $! (RetV (do_natop op n n')) σ'' with "Hσ"). *)
     (* iExists _. *)
     (* iPureIntro. *)
diff --git a/theories/examples/delim_lang/interp.v b/theories/examples/delim_lang/interp.v
index 4255ee6..a3c2bef 100644
--- a/theories/examples/delim_lang/interp.v
+++ b/theories/examples/delim_lang/interp.v
@@ -32,15 +32,15 @@ Section interp.
   (** ** RESET *)
 
   Program Definition interp_reset {S} (e : S -n> IT) : S -n> IT :=
-    λne env, RESET (Next $ e env).
+    λne env, RESET (laterO_map 𝒫 (Next $ e env)).
   Solve All Obligations with solve_proper.
 
   (** ** SHIFT *)
 
   Program Definition interp_shift {S} (e : @interp_scope F R _ (inc S) -n> IT) :
     interp_scope S -n> IT :=
-    λne env, SHIFT (λne (k : laterO IT -n> laterO IT),
-                      Next (e (extend_scope env (λit x, Tau (k (Next x)))))).
+    λne env, SHIFT (laterO_map 𝒫 ◎ (λne (k : laterO IT -n> laterO IT),
+                      (Next (e (extend_scope env (λit x, Tau (k (Next x)))))))).
   Next Obligation. solve_proper. Defined.
   Next Obligation.
     solve_proper_prepare.
@@ -292,7 +292,6 @@ Section interp.
     intros S C v mk <- n???. by repeat f_equiv.
   Qed.
 
-
   Global Instance interp_val_asval {S} {D : interp_scope S} (v : val S)
     : AsVal (interp_val v D).
   Proof.
@@ -430,8 +429,6 @@ Section interp.
       + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv.
   Qed.
 
-
-
   (** ** Interpretation of continuations is a homormophism *)
 
   #[local] Instance interp_cont_hom_emp {S} env :
@@ -552,270 +549,268 @@ Section interp.
     induction K; simpl; apply _.
   Qed.
 
-  (** ** Finally, preservation of reductions *)
-  Lemma interp_cred_no_reify {S : Set} (env : interp_scope S) (C C' : config S)
-    (t t' : IT) (σ σ' : state) n :
-    C ===> C' / (n, 0) ->
-    (interp_config C env) = (t, σ) ->
-    (interp_config C' env) = (t', σ') ->
-    t ≡ Tick_n n $ t'.
-  Proof.
-    inversion 1; cbn-[IF APP' Tick get_ret2]; intros Ht Ht'; inversion Ht; inversion Ht'; try done.
-    - do 4 f_equiv. intro. simpl. by repeat f_equiv.
-    - rewrite -hom_tick. f_equiv.
-      erewrite APP_APP'_ITV; last apply _.
-      trans (interp_cont k env (APP (Fun (Next (ir_unf (interp_expr e) env))) (Next $ interp_val v env))).
-      { repeat f_equiv. apply interp_rec_unfold. }
-      rewrite APP_Fun. simpl. rewrite hom_tick. do 2 f_equiv.
-      simplify_eq.
-      rewrite !interp_expr_subst.
-      f_equiv.
-      intros [| [| x]]; simpl; [| reflexivity | reflexivity].
-      rewrite interp_val_ren.
-      f_equiv.
-      intros ?; simpl; reflexivity.
-    (* - rewrite get_val_ITV. *)
-    (*   simpl. *)
-    (*   rewrite get_fun_fun. *)
-    (*   simpl. *)
-    (*   rewrite <-Tick_eq. *)
-    (*   rewrite hom_tick. *)
-    (*   rewrite hom_tick. *)
-    (*   rewrite hom_tick. *)
-    (*   rewrite hom_tick. *)
-
-    - subst.
-      destruct n0; simpl.
-      + by rewrite IF_False; last lia.
-      + by rewrite IF_True; last lia.
-    - do 2 f_equiv. simplify_eq.
-      destruct v1,v0; try naive_solver. simpl in *.
-      rewrite NATOP_Ret.
-      destruct op; simplify_eq/=; done.
-  Qed.
+  (* (** ** Finally, preservation of reductions *) *)
+  (* Lemma interp_cred_no_reify {S : Set} (env : interp_scope S) (C C' : config S) *)
+  (*   (t t' : IT) (σ σ' : state) n : *)
+  (*   C ===> C' / (n, 0) -> *)
+  (*   (interp_config C env) = (t, σ) -> *)
+  (*   (interp_config C' env) = (t', σ') -> *)
+  (*   t ≡ Tick_n n $ t'. *)
+  (* Proof. *)
+  (*   inversion 1; cbn-[IF APP' Tick get_ret2]; intros Ht Ht'; inversion Ht; inversion Ht'; try done. *)
+  (*   - do 4 f_equiv. intro. simpl. by repeat f_equiv. *)
+  (*   - rewrite -hom_tick. f_equiv. *)
+  (*     erewrite APP_APP'_ITV; last apply _. *)
+  (*     trans (interp_cont k env (APP (Fun (Next (ir_unf (interp_expr e) env))) (Next $ interp_val v env))). *)
+  (*     { repeat f_equiv. apply interp_rec_unfold. } *)
+  (*     rewrite APP_Fun. simpl. rewrite hom_tick. do 2 f_equiv. *)
+  (*     simplify_eq. *)
+  (*     rewrite !interp_expr_subst. *)
+  (*     f_equiv. *)
+  (*     intros [| [| x]]; simpl; [| reflexivity | reflexivity]. *)
+  (*     rewrite interp_val_ren. *)
+  (*     f_equiv. *)
+  (*     intros ?; simpl; reflexivity. *)
+  (*   (* - rewrite get_val_ITV. *) *)
+  (*   (*   simpl. *) *)
+  (*   (*   rewrite get_fun_fun. *) *)
+  (*   (*   simpl. *) *)
+  (*   (*   rewrite <-Tick_eq. *) *)
+  (*   (*   rewrite hom_tick. *) *)
+  (*   (*   rewrite hom_tick. *) *)
+  (*   (*   rewrite hom_tick. *) *)
+  (*   (*   rewrite hom_tick. *) *)
+  (*   - subst. *)
+  (*     destruct n0; simpl. *)
+  (*     + by rewrite IF_False; last lia. *)
+  (*     + by rewrite IF_True; last lia. *)
+  (*   - do 2 f_equiv. simplify_eq. *)
+  (*     destruct v1,v0; try naive_solver. simpl in *. *)
+  (*     rewrite NATOP_Ret. *)
+  (*     destruct op; simplify_eq/=; done. *)
+  (* Qed. *)
 
-  Lemma interp_cred_no_reify_state {S : Set} (env : interp_scope S) (C C' : config S)
-    (t t' : IT) (σ σ' : state) n :
-    C ===> C' / (n, 0) ->
-    (interp_config C env) = (t, σ) ->
-    (interp_config C' env) = (t', σ') ->
-    σ = σ'.
-  Proof.
-    inversion 1; cbn; intros Ht Ht'; inversion Ht; inversion Ht'; subst; reflexivity.
-  Qed.
+  (* Lemma interp_cred_no_reify_state {S : Set} (env : interp_scope S) (C C' : config S) *)
+  (*   (t t' : IT) (σ σ' : state) n : *)
+  (*   C ===> C' / (n, 0) -> *)
+  (*   (interp_config C env) = (t, σ) -> *)
+  (*   (interp_config C' env) = (t', σ') -> *)
+  (*   σ = σ'. *)
+  (* Proof. *)
+  (*   inversion 1; cbn; intros Ht Ht'; inversion Ht; inversion Ht'; subst; reflexivity. *)
+  (* Qed. *)
 
-  Opaque map_meta_cont.
-  Opaque extend_scope.
-
-  Lemma interp_cred_yes_reify {S : Set} (env : interp_scope S) (C C' : config S)
-    (t t' : IT) (σ σ' : state) (σr : gState_rest sR_idx rs ♯ IT) n :
-    C ===> C' / (n, 1) ->
-    (interp_config C env) = (t, σ) ->
-    (interp_config C' env) = (t', σ') ->
-    reify (gReifiers_sReifier rs) t (gState_recomp σr (sR_state σ))
-      ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ t').
-  Proof.
-    inversion 1; cbn-[IF APP' Tick get_ret2 gState_recomp]; intros Ht Ht'; inversion Ht; inversion Ht'; subst;
-      try rewrite !map_meta_cont_cons in Ht, Ht'|-*.
-    - trans (reify (gReifiers_sReifier rs)
-               (RESET_ (laterO_map (𝒫 ◎ (interp_cont k env)))
-               (Next (interp_expr e env)))
-               (gState_recomp σr (sR_state (map_meta_cont mk env)))).
-      {
-        repeat f_equiv. rewrite !hom_vis. simpl. f_equiv.
-        rewrite ccompose_id_l. by intro.
-      }
-      rewrite reify_vis_eq_ctx_dep//; last first.
-      {
-        epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_reset)
-                       (laterO_map 𝒫 (Next (interp_expr e env)))
-                       _ (laterO_map (𝒫 ◎ interp_cont k env)) (map_meta_cont mk env)
-                       (laterO_map (𝒫 ◎ interp_cont k env) :: map_meta_cont mk env) σr) as Hr.
-        simpl in Hr|-*.
-        erewrite <-Hr; last reflexivity.
-        repeat f_equiv; last done.  solve_proper.
-      }
-      f_equiv. by rewrite laterO_map_Next.
-    - remember (map_meta_cont mk env) as σ.
-      match goal with
-      | |- context G [Vis ?o ?f ?κ] => set (fin := f); set (op := o); set (kout := κ)
-      end.
-      trans (reify (gReifiers_sReifier rs)
-               (Vis op fin ((laterO_map (𝒫 ◎ interp_cont k env)) ◎ kout))
-               (gState_recomp σr (sR_state σ))).
-      {
-        repeat f_equiv. rewrite !hom_vis. f_equiv. by intro.
-      }
-      rewrite reify_vis_eq_ctx_dep//; last first.
-      {
-        epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_shift)
-                       _ _ (laterO_map (𝒫 ◎ interp_cont k env))
-                     σ σ σr) as Hr.
-        simpl in Hr|-*.
-        erewrite <-Hr; last reflexivity.
-        repeat f_equiv; last first.
-        - subst kout. by rewrite ccompose_id_l.
-        - subst fin. reflexivity.
-        - solve_proper.
-      }
-      simpl.
-      rewrite -Tick_eq. do 3 f_equiv.
-      rewrite interp_expr_subst.
-      simpl. f_equiv.
-      intros [|s]; simpl; eauto.
-      Transparent extend_scope.
-      simpl. f_equiv. f_equiv. by intro.
-      Opaque extend_scope.
-    - remember (map_meta_cont mk env) as σ.
-      remember (laterO_map (𝒫 ◎ interp_cont k env)) as kk.
-      match goal with
-      | |- context G [ofe_mor_car _ _ (get_fun _)
-                        (ofe_mor_car _ _ Fun ?f)] => set (fin := f)
-      end.
-      (* unfold POP. *)
-      (* match goal with *)
-      (*   |- ofe_mor_car _ _ (ofe_mor_car _ _ _ ?a) _ ≡ _ => *)
-      (*     set (T := a) *)
-      (* end. *)
-      (* eassert (T ≡ _). *)
-      (* { *)
-      (*   subst T. *)
-      (*   rewrite get_val_ITV. *)
-      (*   simpl. *)
-      (*   rewrite get_fun_fun. *)
-      (*   subst fin. *)
-      (*   simpl. *)
-      (*   rewrite <-Tick_eq. *)
-      (*   (* rewrite hom_tick. *) *)
-      (*   (* rewrite hom_tick. *) *)
-      (*   (* rewrite hom_tick. *) *)
-      (*   (* rewrite hom_tick. *) *)
-      (*   reflexivity. *)
-      (* } *)
-      (* trans (reify (gReifiers_sReifier rs) *)
-      (*          (𝒫 (interp_cont k env (Tick (Tick (𝒫 (interp_cont k' env (interp_val v env))))))) *)
-      (*          (gState_recomp σr (sR_state σ))). *)
-      (* { *)
-      (*   now do 2 f_equiv. *)
-      (* } *)
-
-      trans (reify (gReifiers_sReifier rs)
-               (APP_CONT_ (Next (interp_val v env))
-                  fin kk)
-            (gState_recomp σr (sR_state (σ)))).
-      {
-        repeat f_equiv. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl.
-        rewrite !hom_vis. f_equiv. subst kk. rewrite ccompose_id_l. intro. simpl.
-        rewrite laterO_map_compose. done.
-      }
-      rewrite reify_vis_eq_ctx_dep//; last first.
-      {
-        epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_app_cont)
-                       (Next (interp_val v env), fin) _ kk σ (kk :: σ) σr)
-                    as Hr.
-        simpl in Hr|-*.
-        erewrite <-Hr; last reflexivity.
-        repeat f_equiv; eauto. solve_proper.
-      }
-      f_equiv. by rewrite -!Tick_eq.
-      (* admit. *)
-    - remember (map_meta_cont mk env) as σ.
-      trans (reify (gReifiers_sReifier rs) (POP (interp_val v env))
-               (gState_recomp σr (sR_state (laterO_map (𝒫 ◎ interp_cont k env) :: σ)))).
-      {
-        do 2 f_equiv; last repeat f_equiv.
-        apply get_val_ITV.
-      }
-      rewrite reify_vis_eq_ctx_dep//; last first.
-      {
-        epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_pop)
-                       (Next (interp_val v env)) _ _
-                       (laterO_map (𝒫 ◎ interp_cont k env) :: σ) σ σr)
-                       as Hr.
-        simpl in Hr|-*.
-        erewrite <-Hr; last reflexivity.
-        repeat f_equiv; last reflexivity.
-        solve_proper.
-      }
-      f_equiv. rewrite laterO_map_Next -Tick_eq.
-      by f_equiv.
-    - trans (reify (gReifiers_sReifier rs) (POP (interp_val v env))
-               (gState_recomp σr (sR_state []))).
-      {
-        do 2 f_equiv; last first.
-        { f_equiv. by rewrite map_meta_cont_nil. }
-        apply get_val_ITV.
-      }
-      rewrite reify_vis_eq_ctx_dep//; last first.
-      {
-        epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_pop)
-                       (Next (interp_val v env)) _ _
-                       [] [] σr)
-                       as Hr.
-        simpl in Hr|-*.
-        erewrite <-Hr; last reflexivity.
-        repeat f_equiv; last reflexivity.
-        solve_proper.
-      }
-      f_equiv. by rewrite -Tick_eq.
-  Qed.
+  (* Opaque map_meta_cont. *)
+  (* Opaque extend_scope. *)
 
+  (* Lemma interp_cred_yes_reify {S : Set} (env : interp_scope S) (C C' : config S) *)
+  (*   (t t' : IT) (σ σ' : state) (σr : gState_rest sR_idx rs ♯ IT) n : *)
+  (*   C ===> C' / (n, 1) -> *)
+  (*   (interp_config C env) = (t, σ) -> *)
+  (*   (interp_config C' env) = (t', σ') -> *)
+  (*   reify (gReifiers_sReifier rs) t (gState_recomp σr (sR_state σ)) *)
+  (*     ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ t'). *)
+  (* Proof. *)
+  (*   inversion 1; cbn-[IF APP' Tick get_ret2 gState_recomp]; intros Ht Ht'; inversion Ht; inversion Ht'; subst; *)
+  (*     try rewrite !map_meta_cont_cons in Ht, Ht'|-*. *)
+  (*   - trans (reify (gReifiers_sReifier rs) *)
+  (*              (RESET_ (laterO_map (𝒫 ◎ (interp_cont k env))) *)
+  (*              (laterO_map 𝒫 (Next (interp_expr e env)))) *)
+  (*              (gState_recomp σr (sR_state (map_meta_cont mk env)))). *)
+  (*     { *)
+  (*       repeat f_equiv. rewrite !hom_vis. simpl. f_equiv. *)
+  (*       rewrite ccompose_id_l. by intro. *)
+  (*     } *)
+  (*     rewrite reify_vis_eq_ctx_dep//; last first. *)
+  (*     { *)
+  (*       epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_reset) *)
+  (*                      (laterO_map 𝒫 (Next (interp_expr e env))) *)
+  (*                      _ (laterO_map (𝒫 ◎ interp_cont k env)) (map_meta_cont mk env) *)
+  (*                      (laterO_map (𝒫 ◎ interp_cont k env) :: map_meta_cont mk env) σr) as Hr. *)
+  (*       simpl in Hr|-*. *)
+  (*       erewrite <-Hr; last reflexivity. *)
+  (*       repeat f_equiv; last done.  solve_proper. *)
+  (*     } *)
+  (*     f_equiv. by rewrite laterO_map_Next. *)
+  (*   - remember (map_meta_cont mk env) as σ. *)
+  (*     match goal with *)
+  (*     | |- context G [Vis ?o ?f ?κ] => set (fin := f); set (op := o); set (kout := κ) *)
+  (*     end. *)
+  (*     trans (reify (gReifiers_sReifier rs) *)
+  (*              (Vis op fin ((laterO_map (𝒫 ◎ interp_cont k env)) ◎ kout)) *)
+  (*              (gState_recomp σr (sR_state σ))). *)
+  (*     { *)
+  (*       repeat f_equiv. rewrite !hom_vis. f_equiv. by intro. *)
+  (*     } *)
+  (*     rewrite reify_vis_eq_ctx_dep//; last first. *)
+  (*     { *)
+  (*       epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_shift) *)
+  (*                      _ _ (laterO_map (𝒫 ◎ interp_cont k env)) *)
+  (*                    σ σ σr) as Hr. *)
+  (*       simpl in Hr|-*. *)
+  (*       erewrite <-Hr; last reflexivity. *)
+  (*       repeat f_equiv; last first. *)
+  (*       - subst kout. by rewrite ccompose_id_l. *)
+  (*       - subst fin. reflexivity. *)
+  (*       - solve_proper. *)
+  (*     } *)
+  (*     simpl. *)
+  (*     rewrite -Tick_eq. do 3 f_equiv. *)
+  (*     rewrite interp_expr_subst. *)
+  (*     simpl. f_equiv. *)
+  (*     intros [|s]; simpl; eauto. *)
+  (*     Transparent extend_scope. *)
+  (*     simpl. f_equiv. f_equiv. by intro. *)
+  (*     Opaque extend_scope. *)
+  (*   - remember (map_meta_cont mk env) as σ. *)
+  (*     remember (laterO_map (𝒫 ◎ interp_cont k env)) as kk. *)
+  (*     match goal with *)
+  (*     | |- context G [ofe_mor_car _ _ (get_fun _) *)
+  (*                       (ofe_mor_car _ _ Fun ?f)] => set (fin := f) *)
+  (*     end. *)
+  (*     (* unfold POP. *) *)
+  (*     (* match goal with *) *)
+  (*     (*   |- ofe_mor_car _ _ (ofe_mor_car _ _ _ ?a) _ ≡ _ => *) *)
+  (*     (*     set (T := a) *) *)
+  (*     (* end. *) *)
+  (*     (* eassert (T ≡ _). *) *)
+  (*     (* { *) *)
+  (*     (*   subst T. *) *)
+  (*     (*   rewrite get_val_ITV. *) *)
+  (*     (*   simpl. *) *)
+  (*     (*   rewrite get_fun_fun. *) *)
+  (*     (*   subst fin. *) *)
+  (*     (*   simpl. *) *)
+  (*     (*   rewrite <-Tick_eq. *) *)
+  (*     (*   (* rewrite hom_tick. *) *) *)
+  (*     (*   (* rewrite hom_tick. *) *) *)
+  (*     (*   (* rewrite hom_tick. *) *) *)
+  (*     (*   (* rewrite hom_tick. *) *) *)
+  (*     (*   reflexivity. *) *)
+  (*     (* } *) *)
+  (*     (* trans (reify (gReifiers_sReifier rs) *) *)
+  (*     (*          (𝒫 (interp_cont k env (Tick (Tick (𝒫 (interp_cont k' env (interp_val v env))))))) *) *)
+  (*     (*          (gState_recomp σr (sR_state σ))). *) *)
+  (*     (* { *) *)
+  (*     (*   now do 2 f_equiv. *) *)
+  (*     (* } *) *)
+
+  (*     trans (reify (gReifiers_sReifier rs) *)
+  (*              (APP_CONT_ (Next (interp_val v env)) *)
+  (*                 fin kk) *)
+  (*           (gState_recomp σr (sR_state (σ)))). *)
+  (*     { *)
+  (*       repeat f_equiv. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl. *)
+  (*       rewrite !hom_vis. f_equiv. subst kk. rewrite ccompose_id_l. intro. simpl. *)
+  (*       rewrite laterO_map_compose. done. *)
+  (*     } *)
+  (*     rewrite reify_vis_eq_ctx_dep//; last first. *)
+  (*     { *)
+  (*       epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_app_cont) *)
+  (*                      (Next (interp_val v env), fin) _ kk σ (kk :: σ) σr) *)
+  (*                   as Hr. *)
+  (*       simpl in Hr|-*. *)
+  (*       erewrite <-Hr; last reflexivity. *)
+  (*       repeat f_equiv; eauto. solve_proper. *)
+  (*     } *)
+  (*     f_equiv. by rewrite -!Tick_eq. *)
+  (*     (* admit. *) *)
+  (*   - remember (map_meta_cont mk env) as σ. *)
+  (*     trans (reify (gReifiers_sReifier rs) (POP_APPLY (interp_val v env)) *)
+  (*              (gState_recomp σr (sR_state (laterO_map (𝒫 ◎ interp_cont k env) :: σ)))). *)
+  (*     { *)
+  (*       do 2 f_equiv; last repeat f_equiv. *)
+  (*       apply get_val_ITV. *)
+  (*     } *)
+  (*     rewrite reify_vis_eq_ctx_dep//; last first. *)
+  (*     { *)
+  (*       epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_pop_apply) *)
+  (*                      (Next (interp_val v env)) _ _ *)
+  (*                      (laterO_map (𝒫 ◎ interp_cont k env) :: σ) σ σr) *)
+  (*                      as Hr. *)
+  (*       simpl in Hr|-*. *)
+  (*       erewrite <-Hr; last reflexivity. *)
+  (*       repeat f_equiv; last reflexivity. *)
+  (*       solve_proper. *)
+  (*     } *)
+  (*     f_equiv. rewrite laterO_map_Next -Tick_eq. *)
+  (*     by f_equiv. *)
+  (*   - trans (reify (gReifiers_sReifier rs) (POP_APPLY (interp_val v env)) *)
+  (*              (gState_recomp σr (sR_state []))). *)
+  (*     { *)
+  (*       do 2 f_equiv; last first. *)
+  (*       { f_equiv. by rewrite map_meta_cont_nil. } *)
+  (*       apply get_val_ITV. *)
+  (*     } *)
+  (*     rewrite reify_vis_eq_ctx_dep//; last first. *)
+  (*     { *)
+  (*       epose proof (@subReifier_reify sz CtxDep reify_delim rs _ IT _ (op_pop_apply) *)
+  (*                      (Next (interp_val v env)) _ _ *)
+  (*                      [] [] σr) *)
+  (*                      as Hr. *)
+  (*       simpl in Hr|-*. *)
+  (*       erewrite <-Hr; last reflexivity. *)
+  (*       repeat f_equiv; last reflexivity. *)
+  (*       solve_proper. *)
+  (*     } *)
+  (*     f_equiv. by rewrite -Tick_eq. *)
+  (* Qed. *)
 
-  (** * SOUNDNESS *)
-  Lemma soundness {S : Set} (env : interp_scope S) (C C' : config S)
-    (t t' : IT) (σ σ' : state) (σr : gState_rest sR_idx rs ♯ IT) n nm :
-    steps C C' nm ->
-    fst nm = n ->
-    (interp_config C env) = (t, σ) ->
-    (interp_config C' env) = (t', σ') ->
-    ssteps (gReifiers_sReifier rs)
-      t (gState_recomp σr (sR_state σ))
-      t' (gState_recomp σr (sR_state σ')) n.
-  Proof.
-    intros H.
-    revert n t t' σ σ'.
-    induction (H); intros n0 t t' σ σ' Hnm Ht Ht'; subst; simpl.
-    - rewrite Ht' in Ht. constructor; inversion Ht; done.
-    - destruct (interp_config c2 env) as [t2 σ2] eqn:Heqc2.
-      assert ((n', m').1 = n') as Hn' by done.
-      rewrite <-Heqc2 in IHs.
-      specialize (IHs s n' t2 t' σ2 σ' Hn' Heqc2 Ht').
-      inversion H2; subst;
-        try solve [specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H2 Ht Heqc2) as Heq;
-                   specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H2 Ht Heqc2) as <-;
-                   simpl in Heq|-*; rewrite Heq; eapply IHs];
-        try solve
-          [eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done;
-            specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq;
-            cbn in Ht; eapply sstep_reify; last done;
-            inversion Ht; rewrite !hom_vis; done].
-      + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done.
-        specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H2 Ht Heqc2) as Heq.
-        specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H2 Ht Heqc2) as <-.
-        simpl in Heq|-*; rewrite Heq. constructor; eauto.
-      + specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq.
-        simpl in Heq|-*.
-        change (2+n') with (1+(1+n')).
-        eapply ssteps_many; last first.
-        * eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done.
-          eapply sstep_tick; reflexivity.
-        * eapply sstep_reify; last apply Heq.
-          cbn in Ht. inversion Ht.
-          rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl.
-          rewrite !hom_vis. done.
-      + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done.
-        specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq.
-        cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl.
-        eapply sstep_reify; simpl in Heq; last first.
-        * rewrite -Heq. f_equiv. f_equiv. rewrite get_val_ITV. simpl. done.
-        * f_equiv. reflexivity.
-      + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done.
-        specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq.
-        cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl.
-        eapply sstep_reify; simpl in Heq; last first.
-        * rewrite -Heq. repeat f_equiv. by rewrite get_val_ITV.
-        * f_equiv. reflexivity.
-  Qed.
+  (* (** * SOUNDNESS *) *)
+  (* Lemma soundness {S : Set} (env : interp_scope S) (C C' : config S) *)
+  (*   (t t' : IT) (σ σ' : state) (σr : gState_rest sR_idx rs ♯ IT) n nm : *)
+  (*   steps C C' nm -> *)
+  (*   fst nm = n -> *)
+  (*   (interp_config C env) = (t, σ) -> *)
+  (*   (interp_config C' env) = (t', σ') -> *)
+  (*   ssteps (gReifiers_sReifier rs) *)
+  (*     t (gState_recomp σr (sR_state σ)) *)
+  (*     t' (gState_recomp σr (sR_state σ')) n. *)
+  (* Proof. *)
+  (*   intros H. *)
+  (*   revert n t t' σ σ'. *)
+  (*   induction (H); intros n0 t t' σ σ' Hnm Ht Ht'; subst; simpl. *)
+  (*   - rewrite Ht' in Ht. constructor; inversion Ht; done. *)
+  (*   - destruct (interp_config c2 env) as [t2 σ2] eqn:Heqc2. *)
+  (*     assert ((n', m').1 = n') as Hn' by done. *)
+  (*     rewrite <-Heqc2 in IHs. *)
+  (*     specialize (IHs s n' t2 t' σ2 σ' Hn' Heqc2 Ht'). *)
+  (*     inversion H2; subst; *)
+  (*       try solve [specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H2 Ht Heqc2) as Heq; *)
+  (*                  specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H2 Ht Heqc2) as <-; *)
+  (*                  simpl in Heq|-*; rewrite Heq; eapply IHs]; *)
+  (*       try solve *)
+  (*         [eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done; *)
+  (*           specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq; *)
+  (*           cbn in Ht; eapply sstep_reify; last done; *)
+  (*           inversion Ht; rewrite !hom_vis; done]. *)
+  (*     + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. *)
+  (*       specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H2 Ht Heqc2) as Heq. *)
+  (*       specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H2 Ht Heqc2) as <-. *)
+  (*       simpl in Heq|-*; rewrite Heq. constructor; eauto. *)
+  (*     + specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq. *)
+  (*       simpl in Heq|-*. *)
+  (*       change (2+n') with (1+(1+n')). *)
+  (*       eapply ssteps_many; last first. *)
+  (*       * eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. *)
+  (*         eapply sstep_tick; reflexivity. *)
+  (*       * eapply sstep_reify; last apply Heq. *)
+  (*         cbn in Ht. inversion Ht. *)
+  (*         rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl. *)
+  (*         rewrite !hom_vis. done. *)
+  (*     + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. *)
+  (*       specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq. *)
+  (*       cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl. *)
+  (*       eapply sstep_reify; simpl in Heq; last first. *)
+  (*       * rewrite -Heq. f_equiv. f_equiv. rewrite get_val_ITV. simpl. done. *)
+  (*       * f_equiv. reflexivity. *)
+  (*     + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. *)
+  (*       specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq. *)
+  (*       cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl. *)
+  (*       eapply sstep_reify; simpl in Heq; last first. *)
+  (*       * rewrite -Heq. repeat f_equiv. by rewrite get_val_ITV. *)
+  (*       * f_equiv. reflexivity. *)
+  (* Qed. *)
 
   (* Lemma soundness_head_step {S : Set} (env : interp_scope S) (C C' : expr S) *)
   (*   (t t' : IT) (σ σ' : state) (σr : gState_rest sR_idx rs ♯ IT) n : *)
@@ -829,4 +824,4 @@ Section interp.
   (* Admitted. *)
 
 End interp.
-#[global] Opaque SHIFT_ RESET_ POP APP_CONT_.
+#[global] Opaque SHIFT_ RESET_ POP_APPLY APP_CONT_.