diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index 2d08421133fdbe17c967bbb50fb60c3db35e09d0..caf454d758e66676e80bade3c65548b983eab70b 100644
--- a/theories/logrel/term_typing_judgment.v
+++ b/theories/logrel/term_typing_judgment.v
@@ -52,3 +52,17 @@ 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.
diff --git a/theories/logrel/term_typing_rules.v b/theories/logrel/term_typing_rules.v
index 993a84f27a023835a889c49a6e23a25506a8a131..a8fcbbeccff54152073953c4600ec08584f46530 100644
--- a/theories/logrel/term_typing_rules.v
+++ b/theories/logrel/term_typing_rules.v
@@ -108,6 +108,17 @@ Section term_typing_rules.
     iApply ("Hf" $! v with "HA1").
   Qed.
 
+  Lemma ltyped_app_copy Γ1 Γ2 Γ3 e1 e2 A1 A2 :
+    (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 → A2 ⫤ Γ3) -∗
+    Γ1 ⊨ e1 e2 : A2 ⫤ Γ3.
+  Proof.
+    iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
+    wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
+    iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
+  Qed.
+
+
   Lemma ltyped_lam Γ1 Γ2 x e A1 A2 :
     (env_cons x A1 Γ1 ⊨ e : A2 ⫤ []) -∗
     Γ1 ++ Γ2 ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ Γ2.