diff --git a/theories/input_lang_delim/interp.v b/theories/input_lang_delim/interp.v
index 0f74cdb..0b144a9 100644
--- a/theories/input_lang_delim/interp.v
+++ b/theories/input_lang_delim/interp.v
@@ -523,49 +523,49 @@ Section interp.
   Solve All Obligations with first [ solve_proper | solve_proper_please ].
 
 
-  Program Definition interp_outputk {S} : S -n> (S -n> IT) -n> IT :=
-    λne env t, interp_output t env.
+  Program Definition interp_outputk {A} : (A -n> IT) -n> A -n> IT :=
+    λne t env, interp_output t env.
   Solve All Obligations with solve_proper.
 
-  Program Definition interp_apprk {A} (q : A -n> IT) : A -n> (A -n> IT) -n> IT :=
-    λne env t, interp_app q t env.
+  Program Definition interp_apprk {A} (q : A -n> IT) : (A -n> IT) -n> A -n> IT :=
+    λne t env, interp_app q t env.
   Solve All Obligations with solve_proper.
 
-  Program Definition interp_applk {A} (q : A -n> IT) : A -n> (A -n> IT) -n> IT :=
-    λne env t, interp_app t q env.
+  Program Definition interp_applk {A} (q : A -n> IT) : (A -n> IT) -n> A -n> IT :=
+    λne t env, interp_app t q env.
   Solve All Obligations with solve_proper.
 
   Program Definition interp_natoprk {A} (op : nat_op) (q : A -n> IT) :
-    A -n> (A -n> IT) -n> IT :=
-    λne env t, interp_natop op q t env.
+    (A -n> IT) -n> A -n> IT :=
+    λne t env, interp_natop op q t env.
   Solve All Obligations with solve_proper.
 
   Program Definition interp_natoplk {A} (op : nat_op) (q : A -n> IT) :
-    A -n> (A -n> IT) -n> IT :=
-    λne env t, interp_natop op t q env.
+    (A -n> IT) -n> A -n> IT :=
+    λne t env, interp_natop op t q env.
   Solve All Obligations with solve_proper.
 
   Program Definition interp_ifcondk {A} (e1 e2 : A -n> IT) :
-    A -n> (A -n> IT) -n> IT :=
-  λne env b, interp_if b e1 e2 env.
+    (A -n> IT) -n> A -n> IT :=
+  λne b env, interp_if b e1 e2 env.
   Solve All Obligations with solve_proper.
 
   Program Definition interp_iftruek {A} (b e2 : A -n> IT) :
-    A -n> (A -n> IT) -n> IT :=
-  λne env e1, interp_if b e1 e2 env.
+    (A -n> IT) -n> A -n> IT :=
+  λne e1 env, interp_if b e1 e2 env.
   Solve All Obligations with solve_proper.
 
   Program Definition interp_iffalsek {A} (e1 b : A -n> IT) :
-    A -n> (A -n> IT) -n> IT :=
-  λne env e2, interp_if b e1 e2 env.
+    (A -n> IT) -n> A -n> IT :=
+  λne e2 env, interp_if b e1 e2 env.
   Solve All Obligations with solve_proper.
 
-  Program Definition interp_resetk {S} : S -n> (S -n> IT) -n> IT :=
-    λne env t, interp_reset t env.
+  Program Definition interp_resetk {A} : (A -n> IT) -n> A -n> IT :=
+    λne t env, interp_reset t env.
   Solve All Obligations with solve_proper.
 
   Definition interp_ectx_el {S} (C : ectx_el S) :
-    interp_scope S -n> ((interp_scope S -n> IT) -n> IT) :=
+    (interp_scope S -n> IT) -n> (interp_scope S) -n> IT :=
     match C with
     | OutputK => interp_outputk
     | AppRK e1 => interp_apprk (interp_expr e1)
@@ -578,11 +578,24 @@ Section interp.
     | ResetK => interp_resetk
     end.
 
-  Definition interp_ectx {S} (K : ectx S) :
-    interp_scope S -n> (interp_scope S -n> IT) -n> IT :=
-    λne env e,
-      (fold_left (λ k c, λne (e : interp_scope S -n> IT),
-                    (interp_ectx_el c env) (λne env, k e)) K (λne env e, e env)) e.
+
+  Fixpoint interp_ectx {S} (K : ectx S) :
+    interp_scope S → IT → IT :=
+    match K with
+    | [] => λ env, idfun
+    | C :: K => λ (env : interp_scope S) (t : IT),
+                  (interp_ectx K env) (interp_ectx_el C (λne env, t) env)
+    end.
+  #[export] Instance interp_ectx_1_ne {S} (K : ectx S) (env : interp_scope S) :
+    NonExpansive (interp_ectx K env : IT → IT).
+  Proof. solve_proper_prepare.
+         induction K; eauto. 
+
+
+  (* Definition interp_ectx {S} (K : ectx S) : interp_scope S -n> IT -n> IT := *)
+  (*   λne env e, *)
+  (*     (fold_left (λ k c, λne (e : interp_scope S -n> IT), *)
+  (*                   (interp_ectx_el c env) (λne env, k e)) K (λne t : , t)) e. *)
 
   (* Open Scope syn_scope. *)
 
@@ -665,22 +678,22 @@ Section interp.
     (*     intros ?; simpl; repeat f_equiv; first by apply interp_ectx_ren. *)
   Qed.
 
-  Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : ectx S):
-    interp_expr (fill K e) env ≡ (interp_ectx K) env ((interp_expr e) env).
-  Proof.
-    revert env.
-    induction K; simpl; intros env; first reflexivity; try (by rewrite IHK).
-    - repeat f_equiv.
-      by rewrite IHK.
-    - repeat f_equiv.
-      by rewrite IHK.
-    - repeat f_equiv.
-      by rewrite IHK.
-    - repeat f_equiv.
-      intros ?; simpl.
-      repeat f_equiv.
-      by rewrite IHK.
-  Qed.
+  (* Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : ectx S): *)
+  (*   interp_expr (fill K e) env ≡ (interp_ectx K) env ((interp_expr e) env). *)
+  (* Proof. *)
+  (*   revert env. *)
+  (*   induction K; simpl; intros env; first reflexivity; try (by rewrite IHK). *)
+  (*   - repeat f_equiv. *)
+  (*     by rewrite IHK. *)
+  (*   - repeat f_equiv. *)
+  (*     by rewrite IHK. *)
+  (*   - repeat f_equiv. *)
+  (*     by rewrite IHK. *)
+  (*   - repeat f_equiv. *)
+  (*     intros ?; simpl. *)
+  (*     repeat f_equiv. *)
+  (*     by rewrite IHK. *)
+  (* Qed. *)
 
   Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S')
     : interp_scope S := λne x, interp_expr (δ x) env.
@@ -703,34 +716,22 @@ Section interp.
     interp_expr (bind δ e) env ≡ interp_expr e (sub_scope δ env)
   with interp_val_subst {S S'} (env : interp_scope S')
          (δ : S [⇒] S') e :
-    interp_val (bind δ e) env ≡ interp_val e (sub_scope δ env)
-  with interp_ectx_subst {S S'} (env : interp_scope S')
-         (δ : S [⇒] S') e :
-    interp_ectx (bind δ e) env ≡ interp_ectx e (sub_scope δ env).
+    interp_val (bind δ e) env ≡ interp_val e (sub_scope δ env).
+  (* with interp_ectx_subst {S S'} (env : interp_scope S') *)
+  (*        (δ : S [⇒] S') e : *)
+  (*   interp_ectx (bind δ e) env ≡ interp_ectx e (sub_scope δ env). *)
   Proof.
-    - destruct e; simpl.
-      + by apply interp_val_subst.
-      + term_simpl.
-        reflexivity.
-      + repeat f_equiv; by apply interp_expr_subst.
-      + repeat f_equiv; by apply interp_expr_subst.
-      + repeat f_equiv; by apply interp_expr_subst.
-      + f_equiv.
-      + repeat f_equiv; by apply interp_expr_subst.
-      + repeat f_equiv.
-        intros ?; simpl.
-        repeat f_equiv.
-        rewrite interp_expr_subst.
+    - destruct e; simpl; try by repeat f_equiv.
+      repeat f_equiv.
+      intros ?; simpl.
+      repeat f_equiv.
+      rewrite interp_expr_subst.
+      f_equiv.
+      intros [| x']; simpl.
+      + reflexivity.
+      + rewrite interp_expr_ren.
         f_equiv.
-        intros [| x']; simpl.
-        * reflexivity.
-        * rewrite interp_expr_ren.
-          f_equiv.
-          intros ?; reflexivity.
-      + repeat f_equiv.
-        * intros ?; simpl.
-          repeat f_equiv; first by apply interp_expr_subst.
-        * by apply interp_expr_subst.
+        intros ?; reflexivity.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_subst.
@@ -752,193 +753,193 @@ Section interp.
           iApply internal_eq_pointwise.
           iIntros (z).
           done.
-      + repeat f_equiv; intro; simpl; repeat f_equiv.
-        by apply interp_ectx_subst.
-    - destruct e; simpl; intros ?; simpl.
-      + reflexivity.
-      + repeat f_equiv; by apply interp_ectx_subst.
-      + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_expr_subst | by apply interp_expr_subst].
-      + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst].
-      + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst].
-      + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst].
-      + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst].
-      + repeat f_equiv; last by apply interp_ectx_subst.
-        intros ?; simpl; repeat f_equiv; first by apply interp_expr_subst.
-      + repeat f_equiv; last by apply interp_val_subst.
-        intros ?; simpl; repeat f_equiv; first by apply interp_ectx_subst.
+    (*   + repeat f_equiv; intro; simpl; repeat f_equiv. *)
+    (*     by apply interp_ectx_subst. *)
+    (* - destruct e; simpl; intros ?; simpl. *)
+    (*   + reflexivity. *)
+    (*   + repeat f_equiv; by apply interp_ectx_subst. *)
+    (*   + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_expr_subst | by apply interp_expr_subst]. *)
+    (*   + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. *)
+    (*   + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst]. *)
+    (*   + repeat f_equiv; [by apply interp_expr_subst | by apply interp_ectx_subst]. *)
+    (*   + repeat f_equiv; [by apply interp_ectx_subst | by apply interp_val_subst]. *)
+    (*   + repeat f_equiv; last by apply interp_ectx_subst. *)
+    (*     intros ?; simpl; repeat f_equiv; first by apply interp_expr_subst. *)
+    (*   + repeat f_equiv; last by apply interp_val_subst. *)
+    (*     intros ?; simpl; repeat f_equiv; first by apply interp_ectx_subst. *)
   Qed.
 
   (** ** Interpretation is a homomorphism (for some constructors) *)
 
-  #[global] Instance interp_ectx_hom_emp {S} env :
-    IT_hom (interp_ectx (EmptyK : ectx S) env).
-  Proof.
-    simple refine (IT_HOM _ _ _ _ _); intros; auto.
-    simpl. fold (@idfun IT). f_equiv. intro. simpl.
-    by rewrite laterO_map_id.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_emp {S} env : *)
+  (*   IT_hom (interp_ectx (EmptyK : ectx S) env). *)
+  (* Proof. *)
+  (*   simple refine (IT_HOM _ _ _ _ _); intros; auto. *)
+  (*   simpl. fold (@idfun IT). f_equiv. intro. simpl. *)
+  (*   by rewrite laterO_map_id. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_output {S} (K : ectx S) env :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (OutputK K) env).
-  Proof.
-    intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - by rewrite !hom_tick.
-    - rewrite !hom_vis.
-      f_equiv. intro. simpl. rewrite -laterO_map_compose.
-      do 2 f_equiv. by intro.
-    - by rewrite !hom_err.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_output {S} (K : ectx S) env : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (OutputK K) env). *)
+  (* Proof. *)
+  (*   intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. *)
+  (*   - by rewrite !hom_tick. *)
+  (*   - rewrite !hom_vis. *)
+  (*     f_equiv. intro. simpl. rewrite -laterO_map_compose. *)
+  (*     do 2 f_equiv. by intro. *)
+  (*   - by rewrite !hom_err. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_if {S}
-    (K : ectx S) (e1 e2 : expr S) env :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (IfK K e1 e2) env).
-  Proof.
-    intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - rewrite -IF_Tick. do 3 f_equiv. apply hom_tick.
-    - assert ((interp_ectx K env (Vis op i ko)) ≡
-        (Vis op i (laterO_map (λne y, interp_ectx K env y) ◎ ko))).
-      { by rewrite hom_vis. }
-      trans (IF (Vis op i (laterO_map (λne y : IT, interp_ectx K env y) ◎ ko))
-               (interp_expr e1 env) (interp_expr e2 env)).
-      { do 3 f_equiv. by rewrite hom_vis. }
-      rewrite IF_Vis. f_equiv. simpl.
-      intro. simpl. by rewrite -laterO_map_compose.
-    - trans (IF (Err e) (interp_expr e1 env) (interp_expr e2 env)).
-      { repeat f_equiv. apply hom_err. }
-      apply IF_Err.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_if {S} *)
+  (*   (K : ectx S) (e1 e2 : expr S) env : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (IfK K e1 e2) env). *)
+  (* Proof. *)
+  (*   intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. *)
+  (*   - rewrite -IF_Tick. do 3 f_equiv. apply hom_tick. *)
+  (*   - assert ((interp_ectx K env (Vis op i ko)) ≡ *)
+  (*       (Vis op i (laterO_map (λne y, interp_ectx K env y) ◎ ko))). *)
+  (*     { by rewrite hom_vis. } *)
+  (*     trans (IF (Vis op i (laterO_map (λne y : IT, interp_ectx K env y) ◎ ko)) *)
+  (*              (interp_expr e1 env) (interp_expr e2 env)). *)
+  (*     { do 3 f_equiv. by rewrite hom_vis. } *)
+  (*     rewrite IF_Vis. f_equiv. simpl. *)
+  (*     intro. simpl. by rewrite -laterO_map_compose. *)
+  (*   - trans (IF (Err e) (interp_expr e1 env) (interp_expr e2 env)). *)
+  (*     { repeat f_equiv. apply hom_err. } *)
+  (*     apply IF_Err. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_appr {S} (K : ectx S)
-    (e : expr S) env :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (AppRK e K) env).
-  Proof.
-    intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - by rewrite !hom_tick.
-    - rewrite !hom_vis. f_equiv. intro x. simpl.
-      by rewrite laterO_map_compose.
-    - by rewrite !hom_err.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_appr {S} (K : ectx S) *)
+  (*   (e : expr S) env : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (AppRK e K) env). *)
+  (* Proof. *)
+  (*   intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. *)
+  (*   - by rewrite !hom_tick. *)
+  (*   - rewrite !hom_vis. f_equiv. intro x. simpl. *)
+  (*     by rewrite laterO_map_compose. *)
+  (*   - by rewrite !hom_err. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_appl {S} (K : ectx S)
-    (v : val S) (env : interp_scope S) :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (AppLK K v) env).
-  Proof.
-    intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - rewrite -APP'_Tick_l. do 2 f_equiv. apply hom_tick.
-    - trans (APP' (Vis op i (laterO_map (interp_ectx K env) ◎ ko))
-               (interp_val v env)).
-      + do 2f_equiv. rewrite hom_vis. do 3 f_equiv. by intro.
-      + rewrite APP'_Vis_l. f_equiv. intro x. simpl.
-        by rewrite -laterO_map_compose.
-    - trans (APP' (Err e) (interp_val v env)).
-      { do 2f_equiv. apply hom_err. }
-      apply APP'_Err_l, interp_val_asval.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_appl {S} (K : ectx S) *)
+  (*   (v : val S) (env : interp_scope S) : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (AppLK K v) env). *)
+  (* Proof. *)
+  (*   intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. *)
+  (*   - rewrite -APP'_Tick_l. do 2 f_equiv. apply hom_tick. *)
+  (*   - trans (APP' (Vis op i (laterO_map (interp_ectx K env) ◎ ko)) *)
+  (*              (interp_val v env)). *)
+  (*     + do 2f_equiv. rewrite hom_vis. do 3 f_equiv. by intro. *)
+  (*     + rewrite APP'_Vis_l. f_equiv. intro x. simpl. *)
+  (*       by rewrite -laterO_map_compose. *)
+  (*   - trans (APP' (Err e) (interp_val v env)). *)
+  (*     { do 2f_equiv. apply hom_err. } *)
+  (*     apply APP'_Err_l, interp_val_asval. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_natopr {S} (K : ectx S)
-    (e : expr S) op env :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (NatOpRK op e K) env).
-  Proof.
-    intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - by rewrite !hom_tick.
-    - rewrite !hom_vis. f_equiv. intro x. simpl.
-      by rewrite laterO_map_compose.
-    - by rewrite !hom_err.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_natopr {S} (K : ectx S) *)
+  (*   (e : expr S) op env : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (NatOpRK op e K) env). *)
+  (* Proof. *)
+  (*   intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. *)
+  (*   - by rewrite !hom_tick. *)
+  (*   - rewrite !hom_vis. f_equiv. intro x. simpl. *)
+  (*     by rewrite laterO_map_compose. *)
+  (*   - by rewrite !hom_err. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_natopl {S} (K : ectx S)
-    (v : val S) op (env : interp_scope S) :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (NatOpLK op K v) env).
-  Proof.
-    intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - rewrite -NATOP_ITV_Tick_l. do 2 f_equiv. apply hom_tick.
-    - trans (NATOP (do_natop op)
-               (Vis op0 i (laterO_map (interp_ectx K env) ◎ ko))
-               (interp_val v env)).
-      { do 2 f_equiv. rewrite hom_vis. f_equiv. by intro. }
-      rewrite NATOP_ITV_Vis_l. f_equiv. intro x. simpl.
-      by rewrite -laterO_map_compose.
-    - trans (NATOP (do_natop op) (Err e) (interp_val v env)).
-      + do 2 f_equiv. apply hom_err.
-      + by apply NATOP_Err_l, interp_val_asval.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_natopl {S} (K : ectx S) *)
+  (*   (v : val S) op (env : interp_scope S) : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (NatOpLK op K v) env). *)
+  (* Proof. *)
+  (*   intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. *)
+  (*   - rewrite -NATOP_ITV_Tick_l. do 2 f_equiv. apply hom_tick. *)
+  (*   - trans (NATOP (do_natop op) *)
+  (*              (Vis op0 i (laterO_map (interp_ectx K env) ◎ ko)) *)
+  (*              (interp_val v env)). *)
+  (*     { do 2 f_equiv. rewrite hom_vis. f_equiv. by intro. } *)
+  (*     rewrite NATOP_ITV_Vis_l. f_equiv. intro x. simpl. *)
+  (*     by rewrite -laterO_map_compose. *)
+  (*   - trans (NATOP (do_natop op) (Err e) (interp_val v env)). *)
+  (*     + do 2 f_equiv. apply hom_err. *)
+  (*     + by apply NATOP_Err_l, interp_val_asval. *)
+  (* Qed. *)
 
-  Lemma get_fun_ret' E A `{Cofe A} n : (∀ f, @get_fun E A _ f (core.Ret n) ≡ Err RuntimeErr).
-  Proof.
-    intros.
-    by rewrite IT_rec1_ret.
-  Qed.
+  (* Lemma get_fun_ret' E A `{Cofe A} n : (∀ f, @get_fun E A _ f (core.Ret n) ≡ Err RuntimeErr). *)
+  (* Proof. *)
+  (*   intros. *)
+  (*   by rewrite IT_rec1_ret. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_throwr {S}
-    (K : ectx S) (v : val S) env :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (ThrowRK v K) env).
-  Proof.
-    intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - pose proof (interp_val_asval v (D := env)).
-      rewrite ->2 get_val_ITV.
-      simpl.
-      rewrite hom_tick.
-      destruct (IT_dont_confuse ((interp_ectx K env α))) as [(e' & HEQ) |[(n & HEQ) |[(f & HEQ) |[(β & HEQ) | (op & i & k & HEQ)]]]].
-      + rewrite HEQ !get_fun_tick !get_fun_err.
-        reflexivity.
-      + rewrite HEQ !get_fun_tick !get_fun_ret'.
-        reflexivity.
-      + rewrite HEQ !get_fun_tick !get_fun_fun//=.
-      + rewrite HEQ !get_fun_tick.
-        reflexivity.
-      + rewrite HEQ !get_fun_tick !get_fun_vis.
-        reflexivity.
-    - pose proof (interp_val_asval v (D := env)).
-      rewrite get_val_ITV.
-      simpl.
-      rewrite hom_vis.
-      rewrite get_fun_vis.
-      f_equiv.
-      intro; simpl.
-      rewrite -laterO_map_compose.
-      repeat f_equiv.
-      intro; simpl.
-      rewrite get_val_ITV.
-      simpl.
-      reflexivity.
-    - pose proof (interp_val_asval v (D := env)).
-      rewrite get_val_ITV.
-      simpl.
-      rewrite hom_err.
-      rewrite get_fun_err.
-      reflexivity.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_throwr {S} *)
+  (*   (K : ectx S) (v : val S) env : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (ThrowRK v K) env). *)
+  (* Proof. *)
+  (*   intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. *)
+  (*   - pose proof (interp_val_asval v (D := env)). *)
+  (*     rewrite ->2 get_val_ITV. *)
+  (*     simpl. *)
+  (*     rewrite hom_tick. *)
+  (*     destruct (IT_dont_confuse ((interp_ectx K env α))) as [(e' & HEQ) |[(n & HEQ) |[(f & HEQ) |[(β & HEQ) | (op & i & k & HEQ)]]]]. *)
+  (*     + rewrite HEQ !get_fun_tick !get_fun_err. *)
+  (*       reflexivity. *)
+  (*     + rewrite HEQ !get_fun_tick !get_fun_ret'. *)
+  (*       reflexivity. *)
+  (*     + rewrite HEQ !get_fun_tick !get_fun_fun//=. *)
+  (*     + rewrite HEQ !get_fun_tick. *)
+  (*       reflexivity. *)
+  (*     + rewrite HEQ !get_fun_tick !get_fun_vis. *)
+  (*       reflexivity. *)
+  (*   - pose proof (interp_val_asval v (D := env)). *)
+  (*     rewrite get_val_ITV. *)
+  (*     simpl. *)
+  (*     rewrite hom_vis. *)
+  (*     rewrite get_fun_vis. *)
+  (*     f_equiv. *)
+  (*     intro; simpl. *)
+  (*     rewrite -laterO_map_compose. *)
+  (*     repeat f_equiv. *)
+  (*     intro; simpl. *)
+  (*     rewrite get_val_ITV. *)
+  (*     simpl. *)
+  (*     reflexivity. *)
+  (*   - pose proof (interp_val_asval v (D := env)). *)
+  (*     rewrite get_val_ITV. *)
+  (*     simpl. *)
+  (*     rewrite hom_err. *)
+  (*     rewrite get_fun_err. *)
+  (*     reflexivity. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom_throwl {S}
-    (K : ectx S) (e : expr S) env :
-    IT_hom (interp_ectx K env) ->
-    IT_hom (interp_ectx (ThrowLK K e) env).
-  Proof.
-    intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl; [by rewrite !hom_tick| | by rewrite !hom_err].
-    rewrite !hom_vis.
-    f_equiv.
-    intro; simpl.
-    rewrite -laterO_map_compose.
-    reflexivity.
-  Qed.
+  (* #[global] Instance interp_ectx_hom_throwl {S} *)
+  (*   (K : ectx S) (e : expr S) env : *)
+  (*   IT_hom (interp_ectx K env) -> *)
+  (*   IT_hom (interp_ectx (ThrowLK K e) env). *)
+  (* Proof. *)
+  (*   intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl; [by rewrite !hom_tick| | by rewrite !hom_err]. *)
+  (*   rewrite !hom_vis. *)
+  (*   f_equiv. *)
+  (*   intro; simpl. *)
+  (*   rewrite -laterO_map_compose. *)
+  (*   reflexivity. *)
+  (* Qed. *)
 
-  #[global] Instance interp_ectx_hom {S}
-    (K : ectx S) env :
-    IT_hom (interp_ectx K env).
-  Proof.
-    induction K; apply _.
-  Qed.
+  (* #[global] Instance interp_ectx_hom {S} *)
+  (*   (K : ectx S) env : *)
+  (*   IT_hom (interp_ectx K env). *)
+  (* Proof. *)
+  (*   induction K; apply _. *)
+  (* Qed. *)
 
   (** ** Finally, preservation of reductions *)
   Lemma interp_expr_head_step {S : Set} (env : interp_scope S) (e : expr S) e' σ σ' K n :
-    head_step e σ e' σ' K (n, 0) →
+    head_step e σ K e' σ' K (n, 0) →
     interp_expr e env ≡ Tick_n n $ interp_expr e' env.
   Proof.
     inversion 1; cbn-[IF APP' INPUT Tick get_ret2].
@@ -966,19 +967,20 @@ Section interp.
       reflexivity.
   Qed.
 
-  Lemma interp_expr_fill_no_reify {S} K (env : interp_scope S) (e e' : expr S) σ σ' n :
-    head_step e σ e' σ' K (n, 0) →
-    interp_expr (fill K e) env
-      ≡
-      Tick_n n $ interp_expr (fill K e') env.
+  Lemma interp_expr_fill_no_reify {S} K K' (env : interp_scope S) (e e' : expr S) σ σ' n :
+    head_step e σ K e' σ' K' (n, 0) →
+    interp_expr (fill K e) env ≡
+      Tick_n n $ interp_expr (fill K' e') env.
   Proof.
+    inversion 1; subst.
+    - eapply sH.
     intros He.
-    rewrite !interp_comp.
-    erewrite <-hom_tick_n.
-    - apply (interp_expr_head_step env) in He.
-      rewrite He.
-      reflexivity.
-    - apply _.
+    (* rewrite !interp_comp. *)
+    (* erewrite <-hom_tick_n. *)
+    (* - apply (interp_expr_head_step env) in He. *)
+    (*   rewrite He. *)
+    (*   reflexivity. *)
+    (* - apply _. *)
   Qed.
 
   Opaque INPUT OUTPUT_ CALLCC CALLCC_ THROW.
diff --git a/theories/input_lang_delim/lang.v b/theories/input_lang_delim/lang.v
index ff0b3e6..0644406 100644
--- a/theories/input_lang_delim/lang.v
+++ b/theories/input_lang_delim/lang.v
@@ -365,7 +365,7 @@ Definition ctx_el_to_expr {X : Set} (K : ectx_el X) (e : expr X) : expr X :=
   | AppRK el => App el e
   | NatOpLK op er => NatOp op e er
   | NatOpRK op el => NatOp op el e
-  | ResetK => e
+  | ResetK => Reset e
   end.
 
 Definition fill {X : Set} (K : ectx X) (e : expr X) : expr X :=
@@ -426,7 +426,7 @@ Definition update_output (n:nat) (s : state) : state :=
 
 
 (** [head_step e σ K e' σ' K' (n, m)] : step from [(e, σ, K)] to [(e', σ', K')] 
-    in [n] ticks with [m] i/o accesses *)
+    in [n] ticks with [m] effects encountered *)
 Variant head_step {S} : expr S → state -> ectx S →
                         expr S → state → ectx S →
                         nat * nat → Prop :=
@@ -453,13 +453,18 @@ Variant head_step {S} : expr S → state -> ectx S →
     n = 0 →
     head_step (If (Val (LitV n)) e1 e2) σ K
       e2 σ K (0, 0)
-  | ValueS v σ K C:
-    head_step (Val v) σ (C::K) (ctx_el_to_expr C (Val v)) σ K (0, 0)
 
   | ShiftS e σ K Ki Ko f:
     ((Ki, Ko) = shift_context K) ->
     f = cont_to_rec Ki ->
-    head_step (Shift e) σ K (subst (Inc := inc) e (Val f)) σ Ko (1, 0).
+    head_step (Shift e) σ K (subst (Inc := inc) e (Val f)) σ Ko (1, 1)
+
+  | ResetS v σ K :
+    head_step (Reset (Val v)) σ K (Val v) σ K (1, 1).
+
+
+  (* | ValueS v σ K C: *)
+  (*   head_step (Val v) σ (C::K) (ctx_el_to_expr C (Val v)) σ K (0, 0) *)
 
   (* | ResetShiftS e σ K E: *)
   (*   head_step *)
@@ -486,7 +491,7 @@ Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
 
 Lemma ctx_el_to_expr_val {S} C (e : expr S) :
   is_Some (to_val (ctx_el_to_expr C e)) → is_Some (to_val e).
-Proof. case : C => [] > H; simpl in H; try by apply is_Some_None in H. done. Qed.
+Proof. case : C => [] > H; simpl in H; try by apply is_Some_None in H. Qed.
 
 Lemma fill_val {S} Ki (e : expr S) :
   is_Some (to_val (fill Ki e)) → is_Some (to_val e).
@@ -845,8 +850,8 @@ Definition compute_head_step {S}
   | (Shift e) =>
       let (Ki, Ko) := shift_context K in
       let f := cont_to_rec Ki in
-      Some ((subst (Inc := inc) e (Val f)), σ, Ko, (1, 0))
-  (* | (Reset (Val v)) => Some (Val v, σ, (1, 0)) *)
+      Some ((subst (Inc := inc) e (Val f)), σ, Ko, (1, 1))
+  | (Reset (Val v)) => Some (Val v, σ, K, (1, 1))
   (* | (Reset (fill E (Shift e))) => None *)
   | _ => None
   end.
@@ -898,4 +903,7 @@ Proof.
   - simpl. 
     destruct (shift_context K) as [Ki Ko] eqn:HK.
     constructor. apply ShiftS with Ki =>//=.
+  -  simpl.
+     destruct e; try (by constructor).
+     do 2 constructor.
 Qed.