diff --git a/_CoqProject b/_CoqProject
index 1edebe4042a1be5df87b93f1ecc0baa43771f35c..c6c303def85db26ec48340b847851d9f77e42307 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,6 +2,8 @@
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/prelude/ctx_subst.v
 theories/prelude/tactics.v
+theories/prelude/asubst.v
+
 theories/logic/spec_ra.v
 theories/logic/spec_rules.v
 theories/logic/model.v
diff --git a/theories/prelude/asubst.v b/theories/prelude/asubst.v
new file mode 100644
index 0000000000000000000000000000000000000000..15e1b7c316f8af8ef059b220808f2bb690ce0305
--- /dev/null
+++ b/theories/prelude/asubst.v
@@ -0,0 +1,21 @@
+(** Autosubst helper lemmata *)
+From stdpp Require Export base numbers.
+From Coq.ssr Require Export ssreflect.
+Global Open Scope general_if_scope.
+(* ^ otherwise ssreflects overwrites `if` *)
+From Autosubst Require Export Autosubst.
+
+Section Autosubst_Lemmas.
+  Context {term : Type} {Ids_term : Ids term}
+          {Rename_term : Rename term} {Subst_term : Subst term}
+          {SubstLemmas_term : SubstLemmas term}.
+
+  Lemma iter_up (m x : nat) (f : var â†’ term) :
+    upn m f x = if decide (x < m) then ids x else rename (+m) (f (x - m)).
+  Proof.
+    revert x; induction m as [|m IH]=> -[|x];
+    repeat (case_match || asimpl || rewrite IH); auto with omega.
+    { exfalso. clear Heqs. revert l. lia. }
+    { exfalso. apply n. lia. }
+  Qed.
+End Autosubst_Lemmas.
diff --git a/theories/prelude/tactics.v b/theories/prelude/tactics.v
index cb2ed338218574d1b2c65474f3849657cb157cfd..067834fceda9317698c017cd4e2075abb48f0d20 100644
--- a/theories/prelude/tactics.v
+++ b/theories/prelude/tactics.v
@@ -1,5 +1,8 @@
 From stdpp Require Export tactics.
 From iris.algebra Require Export ofe.
+From iris.base_logic Require Export base_logic lib.invariants.
+From iris.program_logic Require Import weakestpre.
+Import uPred.
 
 (* Hmmm *)
 Ltac my_prepare :=
@@ -16,3 +19,20 @@ Ltac solve_proper_from_ne :=
     match goal with
     | [H : _ â‰¡ _ |- _] => setoid_rewrite equiv_dist in H; rewrite H
     end] ].
+
+Ltac properness :=
+  repeat match goal with
+  | |- (âˆƒ _: _, _)%I â‰¡ (âˆƒ _: _, _)%I => apply exist_proper =>?
+  | |- (âˆ€ _: _, _)%I â‰¡ (âˆ€ _: _, _)%I => apply forall_proper =>?
+  | |- (_ âˆ§ _)%I â‰¡ (_ âˆ§ _)%I => apply and_proper
+  | |- (_ âˆ¨ _)%I â‰¡ (_ âˆ¨ _)%I => apply or_proper
+  | |- (_ â†’ _)%I â‰¡ (_ â†’ _)%I => apply impl_proper
+  | |- (_ -âˆ— _)%I â‰¡ (_ -âˆ— _)%I => apply wand_proper
+  | |- (WP _ @ _ {{ _ }})%I â‰¡ (WP _ @ _ {{ _ }})%I => apply wp_proper =>?
+  | |- (â–· _)%I â‰¡ (â–· _)%I => apply later_proper
+  | |- (â–¡ _)%I â‰¡ (â–¡ _)%I => apply intuitionistically_proper
+  | |- (|={_,_}=> _ )%I â‰¡ (|={_,_}=> _ )%I => apply fupd_proper
+  | |- (_ âˆ— _)%I â‰¡ (_ âˆ— _)%I => apply sep_proper
+  | |- (inv _ _)%I â‰¡ (inv _ _)%I => apply (contractive_proper _)
+  end.
+
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 00e4fa56cfb8b15d9a8b40376718740bad6a1c07..c92a1ec053f6fb71131e61b6051534a13801e407 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -4,17 +4,15 @@ From iris.algebra Require Export list.
 From iris.proofmode Require Import tactics.
 From reloc.typing Require Export types.
 From reloc.logic Require Import model.
+From reloc.prelude Require Import tactics asubst.
 From Autosubst Require Import Autosubst.
 
 Section semtypes.
   Context `{relocG Î£}.
-
   (** Type-level lambdas are interpreted as closures *)
-
   (** DF: lty2_forall is defined here because it depends on TApp *)
   Definition lty2_forall (C : lty2 â†’ lty2) : lty2 := Lty2 (Î» w1 w2,
     â–¡ âˆ€ A : lty2, interp_expr âŠ¤ (TApp w1) (TApp w2) (C A))%I.
-
   Definition lty2_true : lty2 := Lty2 (Î» w1 w2, True)%I.
 
   Program Definition ctx_lookup (x : var) : listC lty2C -n> lty2C := Î»ne Î”,
@@ -113,53 +111,30 @@ Notation "â¤‰ Î“" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Î“) (at level 1
 
 Section interp_ren.
   Context `{relocG Î£}.
-
-  Import uPred.
-  Ltac properness :=
-    repeat match goal with
-    | |- (âˆƒ _: _, _)%I â‰¡ (âˆƒ _: _, _)%I => apply exist_proper =>?
-    | |- (âˆ€ _: _, _)%I â‰¡ (âˆ€ _: _, _)%I => apply forall_proper =>?
-    | |- (_ âˆ§ _)%I â‰¡ (_ âˆ§ _)%I => apply and_proper
-    | |- (_ âˆ¨ _)%I â‰¡ (_ âˆ¨ _)%I => apply or_proper
-    | |- (_ â†’ _)%I â‰¡ (_ â†’ _)%I => apply impl_proper
-    | |- (_ -âˆ— _)%I â‰¡ (_ -âˆ— _)%I => apply wand_proper
-    | |- (WP _ @ _ {{ _ }})%I â‰¡ (WP _ @ _ {{ _ }})%I => apply wp_proper =>?
-    | |- (â–· _)%I â‰¡ (â–· _)%I => apply later_proper
-    | |- (â–¡ _)%I â‰¡ (â–¡ _)%I => apply intuitionistically_proper
-    | |- (|={_,_}=> _ )%I â‰¡ (|={_,_}=> _ )%I => apply fupd_proper
-    | |- (_ âˆ— _)%I â‰¡ (_ âˆ— _)%I => apply sep_proper
-    | |- (inv _ _)%I â‰¡ (inv _ _)%I => apply (contractive_proper _)
-    end.
-
+  Implicit Types Î” : list lty2.
 
   (* TODO: why do I need to unfold lty2_car here? *)
-  Lemma interp_ren_up Î”1 Î”2 Ï„ Ï„i :
+  Lemma interp_ren_up (Î”1 Î”2 : list lty2) Ï„ Ï„i :
     interp Ï„ (Î”1 ++ Î”2) â‰¡ interp (Ï„.[upn (length Î”1) (ren (+1)%nat)]) (Î”1 ++ Ï„i :: Î”2).
   Proof.
-    revert Î”1 Î”2. induction Ï„ => Î”1 Î”2; simpl; eauto.
-    - intros v1 v2. unfold lty2_car. simpl. properness; eauto.
-        by apply IHÏ„1. by apply IHÏ„2.
-    - intros v1 v2. unfold lty2_car. simpl. properness; eauto.
-        by apply IHÏ„1. by apply IHÏ„2.
-    - intros v1 v2. unfold lty2_car. simpl.
-      unfold interp_expr. properness; eauto.
-        by apply IHÏ„1. by apply IHÏ„2.
+    revert Î”1 Î”2. induction Ï„ => Î”1 Î”2; simpl; eauto;
+    try by
+      (intros ? ?; unfold lty2_car; simpl; properness; repeat f_equiv=>//).
     - apply fixpoint_proper=> Ï„' w1 w2 /=.
       unfold lty2_car. simpl.
       properness; auto. apply (IHÏ„ (_ :: _)).
-    - intros v1 v2; simpl. admit.
-      (* rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl; properness. *)
-      (* { by rewrite !lookup_app_l. } *)
-      (* change (bi_ofeC (uPredI (iResUR Î£))) with (uPredC (iResUR Î£)). *)
-      (* rewrite !lookup_app_r; [|lia ..]. *)
-      (* assert ((length Î”1 + S (x - length Î”1) - length Î”1) = S (x - length Î”1)) as Hwat. *)
-      (* { lia. } *)
-      (* rewrite Hwat. simpl. done. *)
+    - intros v1 v2; simpl.
+      rewrite iter_up. case_decide; simpl; properness.
+      { by rewrite !lookup_app_l. }
+      change (bi_ofeC (uPredI (iResUR Î£))) with (uPredC (iResUR Î£)).
+      rewrite !lookup_app_r; [|lia..].
+      assert ((length Î”1 + S (x - length Î”1) - length Î”1) = S (x - length Î”1))%nat as Hwat.
+      { lia. }
+      rewrite Hwat. simpl. done.
     - intros v1 v2; unfold lty2_car; simpl; unfold interp_expr;
         simpl; properness; auto. apply (IHÏ„ (_ :: _)).
     - intros ??; unfold lty2_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
-    - intros ??; unfold lty2_car; simpl; properness; auto. by apply IHÏ„.
-  Admitted.
+  Qed.
 
   Lemma interp_ren A Î” (Î“ : gmap string type) :
     ((Î» Ï„, interp Ï„ (A::Î”)) <$> â¤‰Î“) â‰¡ ((Î» Ï„, interp Ï„ Î”) <$> Î“).
@@ -170,8 +145,53 @@ Section interp_ren.
     symmetry. apply (interp_ren_up []).
   Qed.
 
+  Lemma interp_weaken (Î”1 Î  Î”2 : list lty2) Ï„ :
+    interp (Ï„.[upn (length Î”1) (ren (+ length Î ))]) (Î”1 ++ Î  ++ Î”2)
+    â‰¡ interp Ï„ (Î”1 ++ Î”2).
+  Proof.
+    revert Î”1 Î  Î”2. induction Ï„=> Î”1 Î  Î”2; simpl; eauto;
+    try by
+      (intros ? ?; simpl; unfold lty2_car; simpl; repeat f_equiv =>//).
+    - apply fixpoint_proper=> Ï„i ?? /=.
+      unfold lty2_car; simpl.
+      properness; auto. apply (IHÏ„ (_ :: _)).
+    - intros ??; simpl; properness; auto.
+      rewrite iter_up; case_decide; properness; simpl.
+      { by rewrite !lookup_app_l. }
+      rewrite !lookup_app_r ;[| lia ..]. do 3 f_equiv. lia.
+    - intros ??; simpl; unfold lty2_car; simpl; unfold interp_expr.
+      properness; auto. by apply (IHÏ„ (_ :: _)).
+    - intros ??; unfold lty2_car; simpl; properness; auto.
+        by apply (IHÏ„ (_ :: _)).
+  Qed.
+
+  Lemma interp_subst_up (Î”1 Î”2 : list lty2) Ï„ Ï„' :
+    interp Ï„ (Î”1 ++ interp Ï„' Î”2 :: Î”2)
+    â‰¡ interp (Ï„.[upn (length Î”1) (Ï„' .: ids)]) (Î”1 ++ Î”2).
+  Proof.
+    revert Î”1 Î”2; induction Ï„=> Î”1 Î”2; simpl; eauto;
+    try by
+      (intros ? ?; unfold lty2_car; simpl; properness; repeat f_equiv=>//).
+    - apply fixpoint_proper=> Ï„i ?? /=.
+      unfold lty2_car. simpl.
+      properness; auto. apply (IHÏ„ (_ :: _)).
+    - intros w1 w2; simpl.
+      rewrite iter_up; case_decide; simpl; properness.
+      { by rewrite !lookup_app_l. }
+      rewrite !lookup_app_r; [|lia..].
+      case EQ: (x - length Î”1)%nat => [|n]; simpl.
+      { symmetry.
+        pose (HW := interp_weaken [] Î”1 Î”2 Ï„' w1 w2).
+        etrans; last by apply HW.
+        asimpl. reflexivity. }
+      rewrite !lookup_app_r; [|lia ..]. repeat f_equiv. lia.
+    - intros ??. unfold lty2_car; simpl; unfold interp_expr.
+      properness; auto. apply (IHÏ„ (_ :: _)).
+    - intros ??; unfold lty2_car; simpl; properness; auto. apply (IHÏ„ (_ :: _)).
+  Qed.
+
   Lemma interp_subst Î”2 Ï„ Ï„' :
     interp Ï„ (interp Ï„' Î”2 :: Î”2) â‰¡ interp (Ï„.[Ï„'/]) Î”2.
-  Proof. Admitted.
+  Proof. apply (interp_subst_up []). Qed.
 
 End interp_ren.