diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 4b5494e99ebb80412b26d4219ec023cafef02acb..f7dac0583a90046c52c585a78fecdbb6c607390f 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -111,7 +111,7 @@ Section fundamental.
     (* TODO better proof here, without exposing interp_expr *)
     iSpecialize ("Hff" with "Hvv"). simpl.
     iApply refines_ret'; eauto.
-  Admitted.
+  Qed.
 
   Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
     □ ({Δ;<[f:=TArrow τ1 τ2]>(<[x:=τ1]>Γ)} ⊨ e ≤log≤ e' : τ2) -∗
@@ -133,15 +133,12 @@ Section fundamental.
     rel_bind_r e1'.
     iApply (refines_bind _ _ _ _ (interp τ1 (R :: Δ)) with "[He1] [He2]").
     - rewrite /bin_log_related.
-      assert (((λ τ : type, (interp τ) (R :: Δ)) <$> ⤉Γ)
-                ≡ ((λ τ : type, (interp τ) Δ) <$> Γ)). admit.
-      (* rewrite H0. *)
-      (* TODO *) admit.
+      by rewrite interp_ren.
     - iIntros (? ?) "? /=".
       rel_pure_l. rel_rec_l.
       rel_pure_r. rel_rec_r.
       done.
-  Admitted.
+  Qed.
 
   (* TODO
   Lemma bin_log_related_seq' Δ Γ e1 e2 e1' e2' τ1 τ2 :
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 4268c8507089ae6274a1ecfc94fbc1313ee41dd1..2d79b913f59343844cf83e0caea7af3fdd8f4833 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -110,3 +110,63 @@ Section props.
 End props.
 
 Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)%nat) <$> Γ) (at level 10, format "⤉ Γ").
+
+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.
+
+
+  (* TODO: why do I need to unfold lty2_car here? *)
+  Lemma interp_ren_up Δ1 Δ2 τ τ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.
+    - 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; 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.
+
+  Lemma interp_ren A Δ (Γ : gmap string type) :
+    ((λ τ, interp τ (A::Δ)) <$> ⤉Γ) ≡ ((λ τ, interp τ Δ) <$> Γ).
+  Proof.
+    rewrite -map_fmap_compose => x /=.
+    rewrite !lookup_fmap.
+    destruct (Γ !! x); auto; simpl. f_equiv.
+    symmetry. apply (interp_ren_up []).
+  Qed.
+End interp_ren.