diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index caf454d758e66676e80bade3c65548b983eab70b..2d08421133fdbe17c967bbb50fb60c3db35e09d0 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -52,17 +52,3 @@ Proof.
   iDestruct (He $!∅ with "[]") as "He"; first by rewrite /env_ltyped.
   iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
 Qed.
-
-Theorem ltyped_mono `{!heapG Σ} Γ1 Γ1' Γ2 Γ2' e τ1 τ2 :
-  (■ ∀ vs, env_ltyped Γ1 vs -∗ env_ltyped Γ1' vs) -∗
-  (■ ∀ vs, env_ltyped Γ2' vs -∗ env_ltyped Γ2 vs) -∗
-  τ1 <: τ2 -∗ (Γ1' ⊨ e : τ1 ⫤ Γ2') -∗ (Γ1 ⊨ e : τ2 ⫤ Γ2).
-Proof.
-  iIntros "#HΓ1 #HΓ2 #Hle #Hltyped" (vs) "!> Henv".
-  iDestruct ("HΓ1" with "Henv") as "Henv".
-  iDestruct ("Hltyped" with "Henv") as "Hltyped'".
-  iApply (wp_wand with "Hltyped'").
-  iIntros (v) "[H1 Henv]".
-  iDestruct ("HΓ2" with "Henv") as "Henv".
-  iFrame "Henv". by iApply "Hle".
-Qed.