the weakening lemma is not needed since it is assumed in the rules of

the type judgement :)

diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index 22abcfa3c29f430820c556546fb64b5b0c9f2ad0..5aada70ca35f539285e200db1794f7ef2e484f64 100644 (file)
--- 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.