Added stronger lemma for framing judgement

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.

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.