From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 22 Mar 2011 20:34:05 +0000 (+0000)
Subject: the thinning lemma follows immediately from the substitution lemma ...
X-Git-Tag: make_still_working~2552
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=019e06780b45d2a0f36fb276768adfe773771780;p=helm.git

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 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.