the thinning lemma follows immediately from the substitution lemma ...

diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index dd730bf3be9b503b270f5853ac72bdfbc93e7bf0..22abcfa3c29f430820c556546fb64b5b0c9f2ad0 100644 (file)
--- a/matita/matita/lib/lambda/types.ma
+++ b/matita/matita/lib/lambda/types.ma
@@ -212,9 +212,11 @@ theorem substitution_tj:
   ]
 qed.
 
+lemma tj_subst_0: ∀G,v,w. G ⊢ v : w → ∀t,u. w :: G ⊢ t : u →
+                  G ⊢ t[0≝v] : u[0≝v].
+#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.
-
-
-(* thinning lemma: special case *)
-axiom tj_thin_1: ∀w,G,t,u. w :: G ⊢ lift t 0 1 : lift u 0 1 → G ⊢ t : u.