From 4478acc3e2f9f9e953eb24d3815e3b1d7ac4b030 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 22 Mar 2011 21:00:04 +0000
Subject: [PATCH] the weakening lemma is not needed since it is assumed in the
 rules of the type judgement :)

---
 matita/matita/lib/lambda/types.ma | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index 22abcfa3c..5aada70ca 100644
--- a/matita/matita/lib/lambda/types.ma
+++ b/matita/matita/lib/lambda/types.ma
@@ -217,6 +217,3 @@ lemma tj_subst_0: ∀G,v,w. G ⊢ v : w → ∀t,u. w :: G ⊢ t : u →
 #G #v #w #Hv #t #u #Ht 
 lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
 qed.
-
-(* weakening lemma: special case *)
-axiom tj_weak_1: ∀G,t,u. G ⊢ t : u → ∀w. w :: G ⊢ lift t 0 1 : lift u 0 1.
-- 
2.39.2