From 98c1df36c2b0e450f8f8dd10fdf3c7634bd9b4cc Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Thu, 17 Sep 2020 14:06:55 +0200
Subject: [PATCH] Removed redundant monotonicity lemma for typing judgement

---
 theories/logrel/term_typing_judgment.v | 14 --------------
 1 file changed, 14 deletions(-)

diff --git a/theories/logrel/term_typing_judgment.v b/theories/logrel/term_typing_judgment.v
index caf454d..2d08421 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.
-- 
GitLab