diff --git a/theories/examples/delim_lang/adeq.v b/theories/examples/delim_lang/adeq.v
index 60d1f46..aa415b5 100644
--- a/theories/examples/delim_lang/adeq.v
+++ b/theories/examples/delim_lang/adeq.v
@@ -5,7 +5,7 @@ From iris.algebra Require Import list.
 From iris.proofmode Require Import classes tactics.
 From iris.base_logic Require Import algebra.
 
-(* TODO: typing rules, if, compat for contexts, binary relation *)
+(* TODO: typing rules, compat for contexts, binary relation *)
 
 Require Import Binding.Lib Binding.Set Binding.Env.
 
@@ -18,68 +18,75 @@ Inductive ty :=
 
 Declare Scope types.
 
-(* Notation "τ '∕' α '→' σ '∕' β" := (Tarr τ α σ β) (at level 60) : types. *)
-(* Notation "'Cont' τ σ" := (Tcont τ σ) (at level 60) : types. *)
-
-(* Reserved Notation "Γ ';' α '⊢ₑ' e ':' τ ';' β" *)
-(*   (at level 90, e at next level, τ at level 20, no associativity). *)
-
-(* Reserved Notation "Γ ';' α '⊢ᵥ' e ':' τ ';' β" *)
-(*   (at level 90, e at next level, τ at level 20, no associativity). *)
-
-(* Reserved Notation "Γ ';' α '⊢ᵪ' e ':' τ ';' β" *)
-(*   (at level 90, e at next level, τ at level 20, no associativity). *)
-
-(* TODO: pure stuff has ∀ σ deeper inside *)
-(* Inductive typed_expr {S : Set} (Γ : S -> ty) : ty -> expr S -> ty -> ty -> Prop := *)
-(* | typed_Val v α τ β : *)
-(*   (Γ; α ⊢ᵥ v : τ; β) → *)
-(*   (Γ; α ⊢ₑ v : τ; β) *)
-(* | typed_Var x τ α : *)
-(*   (Γ x = τ) → *)
-(*   (Γ; α ⊢ₑ (Var x) : τ; α) *)
-(* | typed_App e₁ e₂ γ α β δ σ τ : *)
-(*   (Γ; γ ⊢ₑ e₁ : (Tarr σ α τ β); δ) → *)
-(*   (Γ; β ⊢ₑ e₂ : σ; γ) → *)
-(*   (Γ; α ⊢ₑ (App e₁ e₂) : τ; δ) *)
-(* | typed_AppCont e₁ e₂ α β δ σ τ : *)
-(*   (Γ; δ ⊢ₑ e₁ : (Tcont τ α); β) → *)
-(*   (Γ; σ ⊢ₑ e₂ : τ; δ) → *)
-(*   (Γ; σ ⊢ₑ (AppCont e₁ e₂) : α; β) *)
-(* | typed_NatOp o e₁ e₂ α β : *)
-(*   (Γ; α ⊢ₑ e₁ : Tnat; β) → *)
-(*   (Γ; α ⊢ₑ e₂ : Tnat; β) → *)
-(*   (Γ; α ⊢ₑ NatOp o e₁ e₂ : Tnat; β) *)
-(* | typed_If e e₁ e₂ α β σ τ : *)
-(*   (Γ; σ ⊢ₑ e : Tnat; β) → *)
-(*   (Γ; α ⊢ₑ e₁ : τ; σ) → *)
-(*   (Γ; α ⊢ₑ e₂ : τ; σ) → *)
-(*   (Γ; α ⊢ₑ (if e then e₁ else e₂) : τ; β) *)
-(* | typed_Shift (e : @expr (inc S)) τ α σ β : *)
-(*   (Γ ▹ (Tcont τ α); σ ⊢ₑ e : σ; β) → *)
-(*   (Γ; α ⊢ₑ Shift e : τ; β) *)
-(* | typed_Reset e α σ τ : *)
-(*   (Γ; σ ⊢ₑ e : σ; τ) → *)
-(*   (Γ; α ⊢ₑ reset e : τ; α) *)
-(* where "Γ ';' α '⊢ₑ' e ':' τ ';' β" := (typed_expr Γ α e τ β) : types *)
-(* with typed_val {S : Set} (Γ : S -> ty) : ty -> val S -> ty -> ty -> Prop := *)
-(* | typed_LitV n α : *)
-(*   (Γ; α ⊢ᵥ #n : Tnat; α) *)
-(* | typed_RecV (e : expr (inc (inc S))) (δ σ τ α β : ty) : *)
-(*   ((Γ ▹ (Tarr σ α τ β) ▹ σ); α ⊢ₑ e : τ; β) -> *)
-(*   (Γ; δ ⊢ᵥ (RecV e) : (Tarr σ α τ β); δ) *)
-(* | typed_ContV (k : cont S) τ α β : *)
-(*   (Γ; α ⊢ᵪ k : τ; β) → *)
-(*   (Γ; α ⊢ᵥ (ContV k) : τ; β) *)
-(* where "Γ ';' α '⊢ᵥ' e ':' τ ';' β" := (typed_val Γ α e τ β) : types *)
-(* with typed_cont {S : Set} (Γ : S -> ty) : ty -> cont S -> ty -> ty -> Prop := *)
-(* | typed_END τ δ : *)
-(*   (Γ; δ ⊢ᵪ END : (Tcont τ τ); δ) *)
-(* | typed_IfK e₁ e₂ α β δ A k τ : *)
-(*   (Γ; α ⊢ₑ e₁ : τ; β) -> *)
-(*   (Γ; α ⊢ₑ e₂ : τ; β) -> *)
-(*   (Γ; β ⊢ᵪ k : Tcont τ A; δ) -> *)
-(*   (Γ; α ⊢ᵪ IfK e₁ e₂ k : Tcont Tnat A; δ) *)
+Notation "τ '∕' α '→' σ '∕' β" := (Tarr τ α σ β) (at level 60) : types.
+Notation "'Cont' τ σ" := (Tcont τ σ) (at level 60) : types.
+
+Reserved Notation "Γ ';' α '⊢ₑ' e ':' τ ';' β"
+  (at level 90, e at next level, τ at level 20, no associativity).
+
+Reserved Notation "Γ ';' α '⊢ᵥ' e ':' τ ';' β"
+  (at level 90, e at next level, τ at level 20, no associativity).
+
+Reserved Notation "Γ '⊢ᵪ' e ':' τ '⤞' σ"
+  (at level 90, e at next level, τ at level 20, no associativity).
+
+Inductive typed_expr {S : Set} (Γ : S -> ty) : ty -> expr S -> ty -> ty -> Prop :=
+| typed_Val v α τ β :
+  (Γ; α ⊢ᵥ v : τ; β) →
+  (Γ; α ⊢ₑ v : τ; β)
+| typed_Var x τ α :
+  (Γ x = τ) →
+  (Γ; α ⊢ₑ (Var x) : τ; α)
+| typed_App e₁ e₂ γ α β δ σ τ :
+  (Γ; γ ⊢ₑ e₁ : (Tarr σ α τ β); δ) →
+  (Γ; β ⊢ₑ e₂ : σ; γ) →
+  (Γ; α ⊢ₑ (App e₁ e₂) : τ; δ)
+| typed_AppCont e₁ e₂ α β δ σ τ :
+  (Γ; σ ⊢ₑ e₁ : (Tcont τ α); δ) →
+  (Γ; δ ⊢ₑ e₂ : τ; β) →
+  (Γ; σ ⊢ₑ (AppCont e₁ e₂) : α; β)
+| typed_NatOp o e₁ e₂ α β γ :
+  (Γ; α ⊢ₑ e₁ : Tnat; β) →
+  (Γ; β ⊢ₑ e₂ : Tnat; γ) →
+  (Γ; α ⊢ₑ NatOp o e₁ e₂ : Tnat; γ)
+| typed_If e e₁ e₂ α β σ τ :
+  (Γ; β ⊢ₑ e : Tnat; α) →
+  (Γ; σ ⊢ₑ e₁ : τ; β) →
+  (Γ; σ ⊢ₑ e₂ : τ; β) →
+  (Γ; σ ⊢ₑ (if e then e₁ else e₂) : τ; α)
+| typed_Shift (e : @expr (inc S)) τ α σ β :
+  (Γ ▹ (Tcont τ α); σ ⊢ₑ e : σ; β) →
+  (Γ; α ⊢ₑ Shift e : τ; β)
+| typed_Reset e α σ τ :
+  (Γ; σ ⊢ₑ e : σ; τ) →
+  (Γ; α ⊢ₑ reset e : τ; α)
+where "Γ ';' α '⊢ₑ' e ':' τ ';' β" := (typed_expr Γ α e τ β) : types
+with typed_val {S : Set} (Γ : S -> ty) : ty -> val S -> ty -> ty -> Prop :=
+| typed_LitV n α :
+  (Γ; α ⊢ᵥ #n : Tnat; α)
+| typed_RecV (e : expr (inc (inc S))) (δ σ τ α β : ty) :
+  ((Γ ▹ (Tarr σ α τ β) ▹ σ); α ⊢ₑ e : τ; β) ->
+  (Γ; δ ⊢ᵥ (RecV e) : (Tarr σ α τ β); δ)
+| typed_ContV (k : cont S) τ σ α :
+  (Γ ⊢ᵪ k : τ ⤞ σ) →
+  (Γ; α ⊢ᵥ (ContV k) : (Tcont τ σ); α)
+where "Γ ';' α '⊢ᵥ' e ':' τ ';' β" := (typed_val Γ α e τ β) : types
+with typed_cont {S : Set} (Γ : S -> ty) : cont S -> ty -> ty -> Prop :=
+| typed_END τ :
+  (Γ ⊢ᵪ END : τ ⤞ τ)
+| typed_IfK k e₁ e₂ α β τ :
+  (Γ; α ⊢ₑ e₁ : τ; β) ->
+  (Γ; α ⊢ₑ e₂ : τ; β) ->
+  (Γ ⊢ᵪ k : τ ⤞ α) ->
+  (Γ ⊢ᵪ IfK e₁ e₂ k : Tnat ⤞ β)
+| typed_NatOpLK op v k α τ :
+  (Γ; τ ⊢ᵥ v : Tnat; α) ->
+  (Γ ⊢ᵪ k : Tnat ⤞ τ) ->
+  (Γ ⊢ᵪ NatOpLK op v k : Tnat ⤞ α)
+| typed_NatOpRK op e k α τ :
+  (Γ; τ ⊢ₑ e : Tnat; α) ->
+  (Γ ⊢ᵪ k : Tnat ⤞ τ) ->
+  (Γ ⊢ᵪ NatOpRK op e k : Tnat ⤞ α)
 (* (* | typed_AppLK v k α β σ δ τ' τ : *) *)
 (* (*   (Γ; α ⊢ᵥ v : τ'; β) -> *) *)
 (* (*   (Γ; β ⊢ᵪ k : Tcont σ τ; δ) -> *) *)
@@ -90,16 +97,41 @@ Declare Scope types.
 (* (*   (Γ; τ ⊢ᵪ AppContLK v k : τ; τ) *) *)
 (* (* | typed_AppContRK e k τ : *) *)
 (* (*   (Γ; τ ⊢ᵪ AppContRK e k : τ; τ) *) *)
-(* | typed_NatOpLK op v k α β δ τ : *)
-(*   (Γ; α ⊢ᵥ v : Tnat; β) -> *)
-(*   (Γ; β ⊢ᵪ k : Tcont Tnat τ; δ) -> *)
-(*   (Γ; α ⊢ᵪ NatOpLK op v k : Tcont Tnat τ; δ) *)
-(* | typed_NatOpRK op e k α β δ τ : *)
-(*   (Γ; α ⊢ₑ e : Tnat; β) -> *)
-(*   (Γ; β ⊢ᵪ k : Tcont Tnat τ; δ) -> *)
-(*   (Γ; α ⊢ᵪ NatOpRK op e k : Tcont Tnat τ; δ) *)
-(* where "Γ ';' α '⊢ᵪ' e ':' τ ';' β" := (typed_cont Γ α e τ β) : types *)
-(* . *)
+where "Γ '⊢ᵪ' e ':' τ '⤞' σ" := (typed_cont Γ e τ σ) : types
+.
+
+Module Example.
+  Open Scope types.
+
+  Lemma typ_example1 α :
+    empty_env; α ⊢ₑ ((#1) +
+                          (reset
+                             ((#3)
+                              + (shift/cc ((($0) @k #5) + (($0) @k #6))))))
+    : Tnat; α.
+  Proof.
+    eapply typed_NatOp.
+    - apply typed_Val.
+      apply typed_LitV.
+    - eapply typed_Reset.
+      eapply typed_NatOp.
+      + apply typed_Val.
+        apply typed_LitV.
+      + eapply typed_Shift.
+        eapply typed_NatOp.
+        * eapply typed_AppCont.
+          -- apply typed_Var.
+             reflexivity.
+          -- apply typed_Val.
+             apply typed_LitV.
+        * eapply typed_AppCont.
+          -- apply typed_Var.
+             reflexivity.
+          -- apply typed_Val.
+             apply typed_LitV.
+  Qed.
+
+End Example.
 
 Open Scope stdpp_scope.
 
@@ -506,23 +538,44 @@ Section logrel.
     apply _.
   Qed.
 
-  Program Definition AppRSCtx_HOM {S : Set}
+  Program Definition AppLSCtx_HOM {S : Set}
     (α : @interp_scope F R _ S -n> IT)
     (env : @interp_scope F R _ S)
-    : HOM := exist _ (interp_apprk rs α (λne env, idfun) env) _.
+    : HOM := exist _ (interp_applk rs α (λne env, idfun) env) _.
   Next Obligation.
     intros; simpl.
     apply _.
   Qed.
 
-  Program Definition AppLSCtx_HOM {S : Set}
+  Transparent LET.
+  Program Definition AppRSCtx_HOM {S : Set}
     (β : IT) (env : @interp_scope F R _ S)
     (Hv : AsVal β)
-    : HOM := exist _ (interp_applk rs (constO β) (λne env, idfun) env) _.
+    : HOM := exist _ (interp_apprk rs (constO β) (λne env, idfun) env) _.
   Next Obligation.
     intros; simpl.
-    apply _.
+    simple refine (IT_HOM _ _ _ _ _); intros; simpl.
+    - solve_proper_please.
+    - rewrite get_val_ITV.
+      simpl.
+      rewrite get_val_ITV.
+      simpl.
+      rewrite get_val_tick.
+      reflexivity.
+    - rewrite get_val_ITV.
+      simpl.
+      rewrite get_val_vis.
+      do 3 f_equiv.
+      intro; simpl.
+      rewrite get_val_ITV.
+      simpl.
+      reflexivity.
+    - rewrite get_val_ITV.
+      simpl.
+      rewrite get_val_err.
+      reflexivity.
   Qed.
+  Opaque LET.
 
   Lemma compat_nat_op {S : Set} (Γ : S → ty)
     D E F e1 e2 op :
@@ -610,11 +663,15 @@ Section logrel.
     iApply "Hκ".
   Qed.
 
+  (* | typed_App e₁ e₂ γ α β δ σ τ : *)
+  (* (Γ; γ ⊢ₑ e₁ : (Tarr σ α τ β); δ) → *)
+  (* (Γ; β ⊢ₑ e₂ : σ; γ) → *)
+  (* (Γ; α ⊢ₑ (App e₁ e₂) : τ; δ) *)
   Lemma compat_app {S : Set} (Γ : S → ty)
-    A B C D E F e1 e2 :
-    ⊢ valid Γ e1 (Tarr A C B E) E F
-      -∗ valid Γ e2 A F D
-      -∗ valid Γ (interp_app rs e1 e2) B C D.
+    ξ α β δ η τ e1 e2 :
+    ⊢ valid Γ e1 (Tarr η α τ β) ξ δ
+      -∗ valid Γ e2 η β ξ
+      -∗ valid Γ (interp_app rs e1 e2) τ α δ.
   Proof.
     iIntros "#H #G".
     iModIntro.
@@ -623,18 +680,23 @@ Section logrel.
     iIntros (σ) "Hσ Hst".
     rewrite /interp_app //=.
 
-    pose (κ' := (AppRSCtx_HOM e1 γ)).
-    assert ((e1 γ ⊙ (e2 γ)) = ((`κ') (e2 γ))) as ->.
-    { simpl; unfold AppRSCtx. reflexivity. }
-    assert ((`κ) ((`κ') (e2 γ)) = ((`κ) ◎ (`κ')) (e2 γ)) as ->.
+    pose (κ' := (AppLSCtx_HOM e2 γ)).
+    match goal with
+    | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] =>
+        set (F := b)
+    end.
+    assert (LET (e1 γ) F = ((`κ') (e1 γ))) as ->.
+    { simpl; unfold AppLSCtx. reflexivity. }
+    clear F.
+    assert ((`κ) ((`κ') (e1 γ)) = ((`κ) ◎ (`κ')) (e1 γ)) as ->.
     { reflexivity. }
     pose (sss := (HOM_compose κ κ')).
     assert ((`κ ◎ `κ') = (`sss)) as ->.
     { reflexivity. }
 
-    iSpecialize ("G" $! γ with "Hγ").
-    iSpecialize ("G" $! sss).
-    iApply ("G" with "[H] Hσ Hst").
+    iSpecialize ("H" $! γ with "Hγ").
+    iSpecialize ("H" $! sss).
+    iApply ("H" with "[H] Hσ Hst").
 
     iIntros (w).
     iModIntro.
@@ -643,18 +705,22 @@ Section logrel.
     subst sss.
     subst κ'.
     simpl.
+    rewrite LET_Val.
+    cbn [ofe_mor_car].    
 
-    pose (κ'' := (AppLSCtx_HOM (IT_of_V w) γ _)).
-    assert (((`κ) (e1 γ ⊙ (IT_of_V w))) = (((`κ) ◎ (`κ'')) (e1 γ))) as ->.
+    match goal with
+    | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] =>
+        set (F := b)
+    end.
+    pose (κ'' := exist _ (LETCTX F) (LETCTX_Hom F) : HOM).
+    assert (((`κ) (LET (e2 γ) F)) = (((`κ) ◎ (`κ'')) (e2 γ))) as ->.
     { reflexivity. }
     pose (sss := (HOM_compose κ κ'')).
     assert ((`κ ◎ `κ'') = (`sss)) as ->.
     { reflexivity. }
-
-    iSpecialize ("H" $! γ with "Hγ").
-    iSpecialize ("H" $! sss).
-    iApply ("H" with "[] Hm Hst").
-
+    iSpecialize ("G" $! γ with "Hγ").
+    iSpecialize ("G" $! sss).
+    iApply ("G" with "[H] Hm Hst").
     iIntros (v).
     iModIntro.
     iIntros "#Hv".
@@ -662,19 +728,22 @@ Section logrel.
     subst sss.
     subst κ''.
     simpl.
-
-    iDestruct "Hv" as "(%n' & #HEQ & Hv)".
-    iSpecialize ("Hv" $! w with "Hw").
-    iSpecialize ("Hv" $! κ with "Hκ").
-    iSpecialize ("Hv" $! m'' with "Hm Hst").
-    iAssert ((IT_of_V v ⊙ (IT_of_V w))
-               ≡ (Fun n' ⊙ (IT_of_V w)))%I as "#HEQ'".
+    rewrite LET_Val.
+    subst F.
+    cbn [ofe_mor_car].    
+
+    iDestruct "Hw" as "(%n' & #HEQ & Hw)".
+    iSpecialize ("Hw" $! v with "Hv").
+    iSpecialize ("Hw" $! κ with "Hκ").
+    iSpecialize ("Hw" $! m'' with "Hm Hst").
+    iAssert ((IT_of_V w ⊙ (IT_of_V v))
+               ≡ (Fun n' ⊙ (IT_of_V v)))%I as "#HEQ'".
     {
-      iApply (f_equivI (λne x, (x ⊙ (IT_of_V w)))).
+      iApply (f_equivI (λne x, (x ⊙ (IT_of_V v)))).
       iApply "HEQ".
     }
     iRewrite "HEQ'".
-    iApply "Hv".
+    iApply "Hw".
   Qed.
 
   Lemma compat_appcont {S : Set} (Γ : S -> ty) e1 e2 τ α δ β σ :
@@ -775,7 +844,58 @@ Section logrel.
         iIntros "_ Hst".
         iApply ("Hκ" with "Hp Hm Hst").
       }
+  Qed.
+
+  Lemma compat_if {S : Set} (Γ : S -> ty) e e₁ e₂ τ σ α β :
+        ⊢ valid Γ e Tnat β α
+          -∗ valid Γ e₁ τ σ β
+          -∗ valid Γ e₂ τ σ β
+          -∗ valid Γ (interp_if rs e e₁ e₂) τ σ α.
+  Proof.
+    iIntros "#H #G #J".
+    iModIntro.
+    iIntros (γ) "#Henv".
+    iIntros (κ) "#Hκ".
+    iIntros (σ') "Hm Hst".
+    unfold interp_if.
+    cbn [ofe_mor_car].
+    pose (κ' := (IFSCtx_HOM (e₁ γ) (e₂ γ))).
+    assert ((IF (e γ) (e₁ γ) (e₂ γ)) = ((`κ') (e γ))) as -> by reflexivity.
+    assert ((`κ) ((`κ') (e γ)) = ((`κ) ◎ (`κ')) (e γ))
+      as -> by reflexivity.
+    pose (sss := (HOM_compose κ κ')).
+    rewrite (HOM_compose_ccompose κ κ' sss)//.
+
+    iSpecialize ("H" $! γ with "Henv").
+    iSpecialize ("H" $! sss).
+    iApply ("H" with "[] Hm Hst").
 
+    iIntros (v).
+    iModIntro.
+    iIntros "#Hv".
+    iIntros (σ'') "Hm Hst".
+    iDestruct "Hv" as "(%n & #Hv)".
+    iRewrite "Hv".
+    rewrite IT_of_V_Ret.
+    subst sss.
+    subst κ'.
+    simpl.
+    unfold IFSCtx.
+    destruct (decide (0 < n)) as [H|H].
+    - rewrite IF_True//.
+      iApply ("G" $! γ with "Henv [Hκ] Hm Hst").
+      iIntros (w).
+      iModIntro.
+      iIntros "#Hw".
+      iIntros (σ''') "Hm Hst".
+      iApply ("Hκ" with "Hw Hm Hst").
+    - rewrite IF_False//; last lia.
+      iApply ("J" $! γ with "Henv [Hκ] Hm Hst").
+      iIntros (w).
+      iModIntro.
+      iIntros "#Hw".
+      iIntros (σ''') "Hm Hst".
+      iApply ("Hκ" with "Hw Hm Hst").
   Qed.
 
   Program Definition valid_ectx {S : Set}
@@ -789,6 +909,15 @@ Section logrel.
     intros; apply _.
   Qed.
 
+  Lemma compat_end {S : Set} (Γ : S → ty) τ
+    : ⊢ valid_ectx Γ (interp_cont rs END) τ τ.
+  Proof.
+    iIntros (γ).
+    iModIntro.
+    iIntros "#H".
+    iApply compat_HOM_id.
+  Qed.
+
   Lemma compat_natop_r {S : Set} (Γ : S → ty) α τ
     op t (E : interp_scope S -n> IT -n> IT)
     `{∀ γ, IT_hom (E γ)}
@@ -935,19 +1064,54 @@ Section logrel.
     iApply "H".
   Qed.
 
-  (* Lemma compat_app_l {S : Set} (Γ : S → ty) τ α c d e *)
-  (*   (* (t : interp_scope S -n> ITVO) *) t *)
+  Lemma compat_ifk {S : Set} (Γ : S -> ty)
+    (E : interp_scope S -n> IT -n> IT)
+    e₁ e₂
+    `{∀ γ, IT_hom (E γ)}
+    `{∀ γ, IT_hom (interp_ifk rs e₁ e₂ E γ)}
+    (τ α β : ty) :
+    ⊢ valid_ectx Γ E τ α
+      -∗ valid Γ e₁ τ α β
+      -∗ valid Γ e₂ τ α β
+      -∗ valid_ectx Γ (interp_ifk rs e₁ e₂ E) Tnat β.
+  Proof.
+    iIntros "#H #G #J".
+    iModIntro.
+    iIntros (γ) "#Henv".
+    iSpecialize ("H" $! γ with "Henv").
+
+    iIntros (v).
+    iModIntro.
+    iIntros "#Hv".
+    iIntros (σ'') "Hm Hst".
+    iDestruct "Hv" as "(%n & #Hv)".
+    iRewrite "Hv".
+    rewrite IT_of_V_Ret.
+    simpl.
+    destruct (decide (0 < n)) as [?|?].
+    - rewrite IF_True//.
+      iSpecialize ("G" $! γ with "Henv").
+      unshelve iSpecialize ("G" $! (exist _ (E γ) _)).
+      { apply _. }
+      iApply ("G" with "H Hm Hst").
+    - rewrite IF_False//; last lia.
+      iSpecialize ("J" $! γ with "Henv").
+      unshelve iSpecialize ("J" $! (exist _ (E γ) _)).
+      { apply _. }
+      iApply ("J" with "H Hm Hst").
+  Qed.
+
+  (* Lemma compat_appk_r {S : Set} (Γ : S → ty) τ α c d e t *)
   (*   (E : interp_scope S -n> IT -n> IT) *)
   (*   `{∀ γ, IT_hom (E γ)} *)
-  (*   (* `{∀ γ, AsVal (t γ)} *) *)
-  (*   `{∀ γ, IT_hom (interp_app_contlk _ t E γ)} : *)
+  (*   `{∀ γ, IT_hom (interp_app_contrk _ t E γ)} : *)
   (*   ⊢ valid_ectx Γ E τ α *)
   (*     -∗ valid Γ t c d e *)
-  (*     -∗ valid_ectx Γ (interp_app_contlk _ t E) τ α. *)
-  (* Proof.     *)
+  (*     -∗ valid_ectx Γ (interp_app_contrk _ t E) τ α. *)
+  (* Proof. *)
+  (*   Opaque interp_app_cont. *)
   (*   iIntros "#H #G". *)
   (*   iIntros (γ). *)
-  (*   assert (AsVal (t γ)); first admit. *)
   (*   iModIntro. *)
   (*   iIntros "#Hγ". *)
   (*   iIntros (v). *)
@@ -955,23 +1119,46 @@ Section logrel.
   (*   iIntros "#Hv". *)
   (*   iIntros (m) "Hm Hst". *)
   (*   simpl. *)
-  (*   rewrite get_val_ITV. *)
-  (*   simpl. *)
-  (*   iSpecialize ("H" $! γ with "Hγ"). *)
-  (*   iSpecialize ("H" $! v with "Hv"). *)
-  (*   iSpecialize ("H" $! m with "Hm Hst"). *)
-  (*   simpl. *)
 
-  (* Lemma compat_app_r {S : Set} (Γ : S → ty) τ α c d e t *)
+  (*   pose (κ'' := (AppContLSCtx_HOM (IT_of_V v) γ _)). *)
+  (*   set (F := (E γ) _). *)
+  (*   assert (F ≡ (((E γ) ◎ (`κ'')) (t γ))) as ->. *)
+  (*   { *)
+  (*     subst F. simpl. Transparent interp_app_cont. simpl. *)
+  (*     f_equiv. *)
+  (*     rewrite ->2 get_val_ITV. *)
+  (*     simpl. *)
+  (*     reflexivity. *)
+  (*   } *)
+  (*   pose (sss := (HOM_compose (exist _ (E γ) (H _)) κ'')). *)
+  (*   assert (((E γ) ◎ `κ'') = (`sss)) as ->. *)
+  (*   { reflexivity. } *)
+
+  (*   iSpecialize ("G" $! γ with "Hγ"). *)
+  (*   iSpecialize ("G" $! sss). *)
+  (*   iApply ("G" with "[] [] Hst"); *)
+  (*     last admit. *)
+  (*   iIntros (w). *)
+  (*   iModIntro. *)
+  (*   iIntros "#Hw". *)
+  (*   iIntros (m') "Hm Hst".     *)
+  (* Admitted. *)
+
+  (* Lemma compat_appk_l {S : Set} (Γ : S → ty) τ α c d e *)
+  (*   (t : interp_scope S -n> IT) *)
   (*   (E : interp_scope S -n> IT -n> IT) *)
   (*   `{∀ γ, IT_hom (E γ)} *)
-  (*   `{∀ γ, IT_hom (interp_app_contrk _ t E γ)} : *)
+  (*   `{∀ γ, AsVal (t γ)} *)
+  (*   `{∀ γ, IT_hom (interp_app_contlk _ t E γ)} : *)
   (*   ⊢ valid_ectx Γ E τ α *)
   (*     -∗ valid Γ t c d e *)
-  (*     -∗ valid_ectx Γ (interp_app_contrk _ t E) τ α.   *)
+  (*     -∗ valid_ectx Γ (interp_app_contlk _ t E) τ α. *)
   (* Proof. *)
+  (*   Opaque interp_app_cont. *)
   (*   iIntros "#H #G". *)
   (*   iIntros (γ). *)
+  (*   assert (AsVal (t γ)). *)
+  (*   { apply _. } *)
   (*   iModIntro. *)
   (*   iIntros "#Hγ". *)
   (*   iIntros (v). *)
@@ -979,13 +1166,93 @@ Section logrel.
   (*   iIntros "#Hv". *)
   (*   iIntros (m) "Hm Hst". *)
   (*   simpl. *)
-  (*   rewrite get_val_ITV. *)
-  (*   simpl. *)
-  (*   iSpecialize ("H" $! γ with "Hγ"). *)
-  (*   iSpecialize ("H" $! v with "Hv"). *)
-  (*   iSpecialize ("H" $! m with "Hm Hst"). *)
-  (*   simpl. *)
-  (* Qed. *)
+
+  (* Admitted. *)
+
+  Lemma compat_cont {S : Set} (Γ : S -> ty) τ σ
+    (k : interp_scope S -n> IT -n> IT)
+    `{∀ γ : interp_scope S, IT_hom (k γ)}
+    : ⊢ valid_ectx Γ k τ σ
+        -∗ ∀ α, valid Γ (interp_cont_val rs k) (Tcont τ σ) α α.
+  Proof.
+    iIntros "#H".
+    iIntros (α γ).
+    iModIntro.
+    iIntros "#Hγ".
+    iIntros (κ) "Hκ".
+    iIntros (m) "Hm Hst".
+    iSpecialize ("H" $! γ with "Hγ").
+    unfold interp_cont_val.
+    simpl.
+    match goal with
+    | |- context G [ofe_mor_car _ _ Fun ?a] =>
+        set (F := a)
+    end.
+    iSpecialize ("Hκ" $! (FunV F)).
+    iApply ("Hκ" with "[] Hm Hst").
+    iExists (exist _ (k γ) (H _)).
+    iSplit.
+    - subst F.
+      Transparent IT_of_V.
+      simpl.
+      iPureIntro.
+      do 2 f_equiv.
+      intros ?; simpl.
+      rewrite later_map_Next.
+      rewrite Tick_eq.
+      reflexivity.
+    - iModIntro.
+      iApply "H".
+  Qed.
+
+  Open Scope types.
+
+  Lemma fundamental_expr {S : Set} (Γ : S -> ty) τ α β e :
+    Γ; α ⊢ₑ e : τ; β → ⊢ valid Γ (interp_expr rs e) τ α β
+  with fundamental_val {S : Set} (Γ : S -> ty) τ α β v :
+    Γ; α ⊢ᵥ v : τ; β → ⊢ valid Γ (interp_val rs v) τ α β
+  with fundamental_cont {S : Set} (Γ : S -> ty) τ σ κ :
+    Γ ⊢ᵪ κ : τ ⤞ σ → ⊢ valid_ectx Γ (interp_cont rs κ) τ σ.
+  Proof.
+    - intros H.
+      destruct H.
+      + by apply fundamental_val.
+      + subst; iApply compat_var.
+      + iApply compat_app;
+          by iApply fundamental_expr.
+      + iApply compat_appcont;
+          by iApply fundamental_expr.
+      + iApply compat_nat_op;
+          by iApply fundamental_expr.
+      + iApply compat_if;
+          by iApply fundamental_expr.
+      + iApply compat_shift;
+          by iApply fundamental_expr.
+      + iApply (compat_reset with "[]");
+          by iApply fundamental_expr.
+    - intros H.
+      destruct H.
+      + iApply compat_nat.
+      + iApply (compat_recV with "[]");
+          by iApply fundamental_expr.
+      + iPoseProof (fundamental_cont _ _ _ _ _ H) as "H".
+        iDestruct (compat_cont with "H") as "G".
+        iSpecialize ("G" $! α).
+        iApply "G".
+    - intros H.
+      destruct H.
+      + iApply compat_end.
+      + iApply compat_ifk;
+          [ by iApply fundamental_cont
+          | by iApply fundamental_expr
+          | by iApply fundamental_expr].
+      + iApply compat_natop_l;
+          [ by iApply fundamental_cont
+          | by iApply fundamental_val].
+      + iApply compat_natop_r;
+          [ by iApply fundamental_cont
+          | by iApply fundamental_expr].
+  Qed.
 
 End logrel.
 
diff --git a/theories/examples/delim_lang/interp.v b/theories/examples/delim_lang/interp.v
index 0e8fda4..18bbc53 100644
--- a/theories/examples/delim_lang/interp.v
+++ b/theories/examples/delim_lang/interp.v
@@ -111,14 +111,51 @@ Section interp.
     simpl. unfold ir_unf. intro. simpl. reflexivity.
   Qed.
 
-
   (** ** APP *)
+  (* Program Definition interp_app {A} (t1 t2 : A -n> IT) : A -n> IT := *)
+  (*   λne env, get_fun *)
+  (*              (λne (f : laterO (IT -n> IT)), *)
+  (*                get_val (λne x, Tau (laterO_ap f (Next x))) (t2 env)) (t1 env). *)
+  (* Next Obligation. *)
+  (*   solve_proper. *)
+  (* Qed. *)
+  (* Next Obligation. *)
+  (*   intros ????????. *)
+  (*   apply get_val_ne. *)
+  (*   intros ?; simpl. *)
+  (*   f_equiv. *)
+  (*   apply Next_contractive. *)
+  (*   destruct n as [| ?]. *)
+  (*   - apply dist_later_0. *)
+  (*   - apply dist_later_S in H. *)
+  (*     apply dist_later_S. *)
+  (*     by f_equiv. *)
+  (* Qed. *)
+  (* Next Obligation. *)
+  (*   solve_proper_please. *)
+  (* Qed. *)
   Program Definition interp_app {A} (t1 t2 : A -n> IT) : A -n> IT :=
-    λne env, APP' (t1 env) (t2 env).
-  Solve All Obligations with first [ solve_proper | solve_proper_please ].
+    λne env,
+      LET (t1 env) $ λne f,
+      LET (t2 env) $ λne x,    
+      APP' f x.
+  Solve All Obligations with solve_proper_please.
+    
   Global Instance interp_app_ne A : NonExpansive2 (@interp_app A).
-  Proof. solve_proper. Qed.
-  Typeclasses Opaque interp_app.
+  Proof. 
+    solve_proper_prepare.
+    f_equiv.
+    - by f_equiv.
+    - intro; simpl.
+      by do 2 f_equiv.
+  Qed.
+  (* Proof. *)
+  (*   solve_proper_prepare. *)
+  (*   do 2 f_equiv; last done. *)
+  (*   intro; simpl. *)
+  (*   by f_equiv. *)
+  (* Qed.   *)
+  Typeclasses Opaque interp_app.  
 
   (** ** APP_CONT *)
 
@@ -129,22 +166,6 @@ Section interp.
                                (k env))
                      (e env).
   Solve All Obligations with first [ solve_proper | solve_proper_please ].
-
-  (* Program Definition interp_app_cont {A} (k e : A -n> IT) : A -n> IT := *)
-  (*   λne env, get_val (λne x, get_fun *)
-  (*                              (λne (f : laterO (IT -n> IT)), *)
-  (*                                (Tau (laterO_ap f (Next x)))) *)
-  (*                              (k env)) *)
-  (*              (e env). *)
-  (* Next Obligation. *)
-  (*   intros. *)
-  (*   intros ???. *)
-  (*   f_equiv. *)
-  (*   now apply later_ap_ne. *)
-  (* Qed. *)
-  (* Next Obligation. solve_proper_please. Qed. *)
-  (* Next Obligation. solve_proper_please. Qed. *)
-
   Global Instance interp_app_cont_ne A : NonExpansive2 (@interp_app_cont A).
   Proof.
     intros n??????. rewrite /interp_app_cont. intro. simpl.
@@ -178,12 +199,58 @@ Section interp.
   Program Definition interp_apprk {A} (q : A -n> IT) (K : A -n> IT -n> IT) :
     A -n> IT -n> IT :=
     λne env t, (K env) $ interp_app q (λne env, t) env.
-  Solve All Obligations with solve_proper.
+  Next Obligation.
+    solve_proper.
+  Qed.
+  Next Obligation.
+    solve_proper_prepare.
+    do 2 f_equiv.
+    intro; simpl.
+    by do 2 f_equiv.
+  Qed.
+  (* Next Obligation. *)
+  (*   solve_proper_prepare. *)
+  (*   do 3 f_equiv. *)
+  (*   intro; simpl. *)
+  (*   by f_equiv. *)
+  (* Qed. *)
+  Next Obligation.
+    solve_proper_prepare.
+    f_equiv; first solve_proper.
+    f_equiv; first solve_proper.
+    intro; simpl.
+    solve_proper.
+  Qed.
+  (* Next Obligation. *)
+  (*   solve_proper_prepare. *)
+  (*   do 2 f_equiv; [done |  | by f_equiv]. *)
+  (*   f_equiv. *)
+  (*   by intro; simpl. *)
+  (* Qed. *)
 
   Program Definition interp_applk {A} (q : A -n> IT) (K : A -n> IT -n> IT) :
     A -n> IT -n> IT :=
     λne env t, (K env) $ interp_app (λne env, t) q env.
-  Solve All Obligations with solve_proper.
+  Next Obligation.
+    solve_proper.
+  Qed.
+  Next Obligation.
+    solve_proper.
+  Qed.
+  (* Next Obligation. *)
+  (*   intros ????????. *)
+  (*   do 3 f_equiv. *)
+  (*   intro; simpl. *)
+  (*   done. *)
+  (* Qed. *)
+  Next Obligation.
+    solve_proper_prepare.
+    f_equiv; first solve_proper.
+    f_equiv; first solve_proper.
+  Qed.  
+  (* Next Obligation. *)
+  (*   solve_proper_please. *)
+  (* Qed. *)
 
   Program Definition interp_app_contrk {A} (q : A -n> IT) (K : A -n> IT -n> IT) :
     A -n> IT -n> IT :=
@@ -246,8 +313,8 @@ Section interp.
     match K with
     | END => λne env x, x
     | IfK e1 e2 K => interp_ifk (interp_expr e1) (interp_expr e2) (interp_cont K)
-    | AppLK v K => interp_applk (interp_val v) (interp_cont K)
-    | AppRK e K => interp_apprk (interp_expr e) (interp_cont K)
+    | AppLK e K => interp_applk (interp_expr e) (interp_cont K)
+    | AppRK v K => interp_apprk (interp_val v) (interp_cont K)
     | AppContLK v K => interp_app_contlk (interp_val v) (interp_cont K)
     | AppContRK e K => interp_app_contrk (interp_expr e) (interp_cont K)
     | NatOpLK op v K => interp_natoplk op (interp_val v) (interp_cont K)
@@ -327,12 +394,20 @@ Section interp.
     interp_cont (fmap δ K) env ≡ interp_cont K (ren_scope δ env).
   Proof.
     - destruct e; simpl; try by repeat f_equiv.
+      + f_equiv; first by rewrite interp_expr_ren.
+        intro; simpl.
+        f_equiv; by rewrite interp_expr_ren.
+        (* f_equiv; last by rewrite interp_expr_ren. *)
+        (* f_equiv. intro. simpl. by f_equiv. *)
       + f_equiv; last by rewrite interp_expr_ren.
         f_equiv. intro. simpl. by f_equiv.
-      + repeat f_equiv. intro; simpl; repeat f_equiv.
-        rewrite interp_expr_ren. f_equiv.
-        intros [|a]; simpl; last done.
-        by repeat f_equiv.
+      + f_equiv; last eauto. f_equiv. intro. simpl.
+        rewrite !laterO_map_Next.
+        repeat f_equiv.
+        rewrite interp_expr_ren.
+        f_equiv.        
+        intros [| ?]; simpl; first done.
+        reflexivity.        
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_ren.
@@ -354,17 +429,33 @@ Section interp.
         apply interp_cont_ren.
     - destruct K; try solve [simpl; repeat f_equiv; intro; simpl; repeat f_equiv;
         (apply interp_expr_ren || apply interp_val_ren || apply interp_cont_ren)].
-      + intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv.
-        intro. simpl. by repeat f_equiv.
-      + intro. simpl. f_equiv; eauto. do 2 f_equiv.
-        intro. simpl. by repeat f_equiv.
+      + intro. simpl. f_equiv; eauto.
+        f_equiv; first by rewrite interp_val_ren.
+        intro; simpl.
+        reflexivity.
+        (* intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. *)
+        (* intro. simpl. by repeat f_equiv. *)
+      + intro. simpl. f_equiv; eauto.
+        f_equiv.
+        intro; simpl.
+        f_equiv.
+        by rewrite interp_expr_ren.
+        (* intro. simpl. f_equiv; eauto. do 2 f_equiv. *)
+        (* intro. simpl. by repeat f_equiv. *)
+      + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv.
+      + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv.
   Qed.
 
   Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : cont S):
     interp_expr (fill K e) env ≡ (interp_cont K) env ((interp_expr e) env).
   Proof. elim : K e env; eauto.
-         intros. simpl. rewrite H. f_equiv. simpl.
-         do 2 f_equiv. intro. simpl. by repeat f_equiv.
+         - intros. simpl. rewrite H. f_equiv. simpl.
+           f_equiv.
+           intro; simpl.           
+           reflexivity.
+           (* do 2 f_equiv. intro. simpl. by repeat f_equiv. *)
+         - intros. simpl. rewrite H. f_equiv. simpl.
+           do 2 f_equiv. intro. simpl. by repeat f_equiv.         
   Qed.
 
   Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S')
@@ -394,11 +485,20 @@ Section interp.
     interp_cont (bind δ K) env ≡ interp_cont K (sub_scope δ env).
   Proof.
     - destruct e; simpl; try by repeat f_equiv.
+      + f_equiv; first by rewrite interp_expr_subst.
+        intro; simpl.
+        f_equiv; first by rewrite interp_expr_subst.
+      (* f_equiv; last eauto. f_equiv. intro. simpl. by repeat f_equiv. *)
       + f_equiv; last eauto. f_equiv. intro. simpl. by repeat f_equiv.
-      + repeat f_equiv. repeat (intro; simpl; repeat f_equiv).
-        rewrite interp_expr_subst. f_equiv.
-        intros [|a]; simpl; repeat f_equiv. rewrite interp_expr_ren.
-        f_equiv. intro. done.
+      + f_equiv; last eauto. f_equiv. intro. simpl.
+        rewrite !laterO_map_Next.
+        repeat f_equiv.
+        rewrite interp_expr_subst.
+        f_equiv.        
+        intros [| ?]; simpl; first done.
+        rewrite interp_expr_ren.
+        f_equiv.
+        intros ?; simpl; done.
     - destruct e; simpl.
       + reflexivity.
       + clear -interp_expr_subst.
@@ -424,12 +524,21 @@ Section interp.
         by rewrite interp_cont_subst.
     - destruct K; try solve [simpl; repeat f_equiv; intro; simpl; repeat f_equiv;
         (apply interp_expr_subst || apply interp_val_subst || apply interp_cont_subst)].
+      + intro; simpl.
+        f_equiv; first by rewrite interp_cont_subst.
+        f_equiv; first by rewrite interp_val_subst.
+        intro; simpl; reflexivity.
+      (* simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv. *)
+      + intro; simpl.
+        f_equiv; first by rewrite interp_cont_subst.
+        f_equiv.
+        intro; simpl.
+        f_equiv; first by rewrite interp_expr_subst.
+      (* simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv. *)
       + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv.
       + 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 :
@@ -454,37 +563,65 @@ Section interp.
       by rewrite -hom_vis.
     - trans (interp_cont K env (Err e)); first (f_equiv; apply IF_Err).
       apply hom_err.
-  Qed.
+  Qed.  
 
+  Transparent LET.
   #[local] Instance interp_cont_hom_appr {S} (K : cont S)
-    (e : expr S) env :
+    (v : val S) (env : interp_scope S) :
     IT_hom (interp_cont K env) ->
-    IT_hom (interp_cont (AppRK e K) env).
+    IT_hom (interp_cont (AppRK v 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.
+    pose proof (interp_val_asval v (D := env)) as HHH.
+    intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
+    - rewrite <-hom_tick.
+      f_equiv.
+      rewrite ->2 get_val_ITV.
+      simpl.
+      rewrite get_val_tick.
+      reflexivity.
+    - rewrite get_val_ITV.
+      simpl.
+      rewrite ->2 hom_vis.
+      f_equiv.
+      intro; simpl.
+      rewrite <-laterO_map_compose.
+      do 2 f_equiv.
+      intro; simpl.
+      rewrite get_val_ITV.
+      simpl.
+      reflexivity.
+    - rewrite <-hom_err.
+      rewrite get_val_ITV.
+      simpl.
+      f_equiv.
+      rewrite get_val_err.
+      reflexivity.
   Qed.
+  Opaque LET.
 
+  Transparent LET.
   #[local] Instance interp_cont_hom_appl {S} (K : cont S)
-    (v : val S) (env : interp_scope S) :
+    (e : expr S) env :
     IT_hom (interp_cont K env) ->
-    IT_hom (interp_cont (AppLK v K) env).
+    IT_hom (interp_cont (AppLK e K) env).
   Proof.
     intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl.
-    - rewrite -hom_tick. f_equiv. apply APP'_Tick_l. apply interp_val_asval.
-    - trans (Vis op i (laterO_map (λne y,
-        (λne t : IT, interp_cont K env (t ⊙ (interp_val v env)))
-          y) ◎ ko));
-        last (simpl; do 3 f_equiv; by intro).
-      by rewrite -hom_vis.
-    - trans (interp_cont K env (Err e));
-        first (f_equiv; apply APP'_Err_l; apply interp_val_asval).
-      apply hom_err.
+    - rewrite <-hom_tick.
+      f_equiv.
+      rewrite get_val_tick.
+      reflexivity.
+    - rewrite !hom_vis.
+      f_equiv.
+      intro; simpl.
+      rewrite <-laterO_map_compose.
+      reflexivity.
+    - rewrite <-hom_err.
+      f_equiv.
+      rewrite hom_err.
+      rewrite get_val_err.
+      reflexivity.
   Qed.
-
+  Opaque LET.
 
   #[local] Instance interp_cont_hom_app_contr {S} (K : cont S)
     (e : expr S) env :
@@ -547,7 +684,8 @@ Section interp.
     (K : cont S) env :
     IT_hom (interp_cont K env).
   Proof.
-    induction K; simpl; apply _.
+    induction K; simpl; try apply _.
+    by apply interp_cont_hom_appr.
   Qed.
 
   (** ** Finally, preservation of reductions *)
@@ -558,30 +696,39 @@ Section interp.
     (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.
+    inversion 1; cbn-[IF LET APP' Tick get_ret2]; intros Ht Ht'; inversion Ht; inversion Ht'; try done.
+    - do 3 f_equiv.
+      intro; simpl.
+      reflexivity.
     - 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.
+      match goal with
+      | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] =>
+          set (F := b)
+      end.
+      trans (interp_cont k env (LET (Fun (Next (ir_unf (interp_expr e) env))) F)).
+      {
+        do 3 f_equiv.
+        apply interp_rec_unfold.
+      }
+      subst F.
+      rewrite LET_Val.
+      simpl.
+      rewrite LET_Val.
+      simpl.
+      rewrite APP'_Fun_l.
+      rewrite laterO_map_Next.
+      rewrite <-Tick_eq.
+      rewrite hom_tick.
+      do 2 f_equiv.
       simplify_eq.
       rewrite !interp_expr_subst.
+      simpl.
       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.
diff --git a/theories/examples/delim_lang/lang.v b/theories/examples/delim_lang/lang.v
index b533bf9..6ec68c6 100644
--- a/theories/examples/delim_lang/lang.v
+++ b/theories/examples/delim_lang/lang.v
@@ -33,8 +33,8 @@ with val {X : Set} :=
 with cont {X : Set} :=
 | END : cont
 | IfK (e1 : expr) (e2 : expr) : cont -> cont
-| AppLK (v : val) : cont -> cont (* ◻ v *)
-| AppRK (e : expr) : cont -> cont (* e ◻ *)
+| AppRK (v : val) : cont -> cont (* v ◻ *)
+| AppLK (e : expr) : cont -> cont (* ◻ e *)
 | AppContLK (v : val) : cont -> cont (* ◻ v *)
 | AppContRK (e : expr) : cont -> cont (* e ◻ *)
 | NatOpLK (op : nat_op) (v : val) : cont -> cont (* ◻ + v *)
@@ -80,8 +80,8 @@ with kmap {A B : Set} (f : A [→] B) (K : cont A) : cont B :=
    match K with
    | END => END
    | IfK e1 e2 k => IfK (emap f e1) (emap f e2) (kmap f k)
-   | AppLK v k => AppLK (vmap f v) (kmap f k)
-   | AppRK e k => AppRK (emap f e) (kmap f k)
+   | AppLK v k => AppLK (emap f v) (kmap f k)
+   | AppRK e k => AppRK (vmap f e) (kmap f k)
    | AppContLK v k => AppContLK (vmap f v) (kmap f k)
    | AppContRK e k => AppContRK (emap f e) (kmap f k)
    | NatOpLK op v k => NatOpLK op (vmap f v) (kmap f k)
@@ -126,8 +126,8 @@ with kbind {A B : Set} (f : A [⇒] B) (K : cont A) : cont B :=
    match K with
    | END => END
    | IfK e1 e2 k => IfK (ebind f e1) (ebind f e2) (kbind f k)
-   | AppLK v k => AppLK (vbind f v) (kbind f k)
-   | AppRK e k => AppRK (ebind f e) (kbind f k)
+   | AppLK v k => AppLK (ebind f v) (kbind f k)
+   | AppRK e k => AppRK (vbind f e) (kbind f k)
    | AppContLK v k => AppContLK (vbind f v) (kbind f k)
    | AppContRK e k => AppContRK (ebind f e) (kbind f k)
    | NatOpLK op v k => NatOpLK op (vbind f v) (kbind f k)
@@ -309,8 +309,8 @@ Fixpoint fill {X : Set} (K : cont X) (e : expr X) : expr X :=
   match K with
   | IfK e1 e2 K => fill K (If e e1 e2)
   | END => e
-  | AppLK v K => fill K (App e (Val v))
-  | AppRK el K => fill K (App el e)
+  | AppRK v K => fill K (App (Val v) e)
+  | AppLK el K => fill K (App e el)
   | AppContLK v K => fill K (AppCont e (Val v))
   | AppContRK el K => fill K (AppCont el e)
   | NatOpLK op v K => fill K (NatOp op e (Val v))
@@ -339,8 +339,8 @@ Fixpoint cont_compose {S} (K1 K2 : cont S) : cont S :=
   match K2 with
   | END => K1
   | IfK e1 e2 K => IfK e1 e2 (cont_compose K1 K)
-  | AppLK v K => AppLK v (cont_compose K1 K)
-  | AppRK e K => AppRK e (cont_compose K1 K)
+  | AppLK e K => AppLK e (cont_compose K1 K)
+  | AppRK v K => AppRK v (cont_compose K1 K)
   | AppContLK v K => AppContLK v (cont_compose K1 K)
   | AppContRK e K => AppContRK e (cont_compose K1 K)
   | NatOpLK op v K => NatOpLK op v (cont_compose K1 K)
@@ -378,10 +378,10 @@ Variant config {S} : Type :=
 Reserved Notation "c '===>' c' / nm"
   (at level 40, c', nm at level 30).
 
-Variant Cred {S : Set} : config (* * state S *) -> config (* * state S *) -> (nat * nat) -> Prop :=
-
-  (* init *)
-  | Ceval_init : forall (e : expr S) (* σ *),
+Variant Cred {S : Set} : config (* * state S *) -> config (* * state S *)
+                         -> (nat * nat) -> Prop :=
+(* init *)
+| Ceval_init : forall (e : expr S) (* σ *),
   (Cexpr e(* , σ *)) ===> (Ceval e END [](* , σ *)) / (0,0)
 
 (* eval *)
@@ -389,7 +389,7 @@ Variant Cred {S : Set} : config (* * state S *) -> config (* * state S *) -> (na
   (Ceval (Val v) k mk(* , σ *)) ===> (Ccont k v mk(* , σ *)) / (0,0)
 
 | Ceval_app : forall e0 e1 k mk (* σ *),
-  (Ceval (App e0 e1) k mk(* , σ *)) ===> (Ceval e1 (AppRK e0 k) mk(* , σ *)) / (0,0)
+  (Ceval (App e0 e1) k mk(* , σ *)) ===> (Ceval e0 (AppLK e1 k) mk(* , σ *)) / (0,0)
 
 | Ceval_app_cont : forall e0 e1 k mk (* σ *),
   (Ceval (AppCont e0 e1) k mk(* , σ *)) ===> (Ceval e1 (AppContRK e0 k) mk(* , σ *)) / (0,0)
@@ -411,14 +411,14 @@ Variant Cred {S : Set} : config (* * state S *) -> config (* * state S *) -> (na
 | Ccont_end : forall v mk (* σ *),
   (Ccont END v mk(* , σ *)) ===> (Cmcont mk v(* , σ *)) / (0,0)
 
-| Ccont_appr : forall e v k mk (* σ *),
-  (Ccont (AppRK e k) v mk(* , σ *)) ===> (Ceval e (AppLK v k) mk(* , σ *)) / (0, 0)
+| Ccont_appl : forall e v k mk (* σ *),
+  (Ccont (AppLK e k) v mk(* , σ *)) ===> (Ceval e (AppRK v k) mk(* , σ *)) / (0, 0)
 
 | Ccont_app_contr : forall e v k mk (* σ *),
   (Ccont (AppContRK e k) v mk(* , σ *)) ===> (Ceval e (AppContLK v k) mk(* , σ *)) / (0, 0)
 
-| Ccont_appl : forall e v k mk (* σ *),
-  (Ccont (AppLK v k) (RecV e) mk(* , σ *)) ===>
+| Ccont_appr : forall e v k mk (* σ *),
+  (Ccont (AppRK (RecV e) k) v mk(* , σ *)) ===>
     (Ceval (subst (Inc := inc)
               (subst (F := expr) (Inc := inc) e
                  (Val (shift (Inc := inc) v)))
@@ -547,12 +547,12 @@ Global Instance AppNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsS
   __app e₁ e₂ := App (__asSynExpr e₁) (__asSynExpr e₂)
   }.
 
-Global Instance AppNotationLK {S : Set} : AppNotation (cont S) (val S) (cont S) := {
-  __app K v := cont_compose K (AppLK v END)
+Global Instance AppNotationRK {S : Set} : AppNotation (cont S) (val S) (cont S) := {
+  __app K v := cont_compose K (AppRK v END)
   }.
 
-Global Instance AppNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNotation (F S) (cont S) (cont S) := {
-  __app e K := cont_compose K (AppRK (__asSynExpr e) END)
+Global Instance AppNotationLK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNotation (F S) (cont S) (cont S) := {
+  __app e K := cont_compose K (AppLK (__asSynExpr e) END)
   }.
 
 Class AppContNotation (A B C : Type) := { __app_cont : A -> B -> C }.