diff --git a/theories/logic/model.v b/theories/logic/model.v
index 56c8e1cc3f03e03bbc5731c4ce7c1e483ebeb719..7dcfb674588888902085a7780d002f63e79ca3bc 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -163,6 +163,16 @@ Proof.
   - admit.
 Admitted.
 
+(* Hmmm *)
+Instance env_ltyped2_proper `{relocG Σ} :
+  Proper ((≡) ==> (=) ==> (≡)) env_ltyped2.
+Proof.
+  intros Γ Γ' HΓ ? vvs ->.
+  apply equiv_dist=>n.
+  setoid_rewrite equiv_dist in HΓ.
+  by rewrite HΓ.
+Qed.
+
 Section refinement.
   Context `{relocG Σ}.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index f7dac0583a90046c52c585a78fecdbb6c607390f..5e1137cf440d96749a9cfddbe5be4290b8cbf749 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -298,12 +298,12 @@ Section fundamental.
     iModIntro. tp_pure j _. wp_pures. iExists _; iFrame.
     iIntros (A). iDestruct ("H" $! A) as "#H". iAlways.
     iSpecialize ("H" $! vvs with "Hs [HΓ]"); auto.
-    { rewrite -map_fmap_compose /=. admit. }
+    { by rewrite (interp_ren A Δ Γ). }
     iIntros (j' K') "Hj". iModIntro.
     wp_pures. tp_pure j' _.
     iMod ("H" $! j' K' with "Hj") as "H".
     iApply "H".
-  Admitted.
+  Qed.
 
   Lemma bin_log_related_alloc Δ Γ e e' τ :
     ({Δ;Γ} ⊨ e ≤log≤ e' : τ) -∗