From 019e06780b45d2a0f36fb276768adfe773771780 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 22 Mar 2011 20:34:05 +0000
Subject: [PATCH] the thinning lemma follows immediately from the substitution
 lemma ...

---
 matita/matita/lib/lambda/types.ma | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index dd730bf3b..22abcfa3c 100644
--- 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.
-- 
2.39.2