- partial commit of rt_transition ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / lstas / lstas.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc
index 289992d5f5640fb876df5693db42be4d76efe984..e9f0341167e4dc66126c08fc9bfda38f4bfddf93 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lstas/lstas.etc
@@ -21,7 +21,7 @@ include "basic_2/static/sh.ma".
 
 (* activate genv *)
 inductive lstas (h): nat → relation4 genv lenv term term ≝
-| lstas_sort: ∀G,L,d,k. lstas h d G L (⋆k) (⋆((next h)^d k))
+| lstas_sort: ∀G,L,d,s. lstas h d G L (⋆s) (⋆((next h)^d s))
 | lstas_ldef: ∀G,L,K,V,W,U,i,d. ⬇[i] L ≡ K.ⓓV → lstas h d G K V W →
               ⬆[0, i+1] W ≡ U → lstas h d G L (#i) U
 | lstas_zero: ∀G,L,K,W,V,i. ⬇[i] L ≡ K.ⓛW → lstas h 0 G K W V →
@@ -39,20 +39,20 @@ interpretation "nat-iterated static type assignment (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lstas_inv_sort1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀k0. T = ⋆k0 →
-                          U = ⋆((next h)^d k0).
+fact lstas_inv_sort1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀s0. T = ⋆s0 →
+                          U = ⋆((next h)^d s0).
 #h #G #L #T #U #d * -G -L -T -U -d
-[ #G #L #d #k #k0 #H destruct //
-| #G #L #K #V #W #U #i #d #_ #_ #_ #k0 #H destruct
-| #G #L #K #W #V #i #_ #_ #k0 #H destruct
-| #G #L #K #W #V #U #i #d #_ #_ #_ #k0 #H destruct
-| #a #I #G #L #V #T #U #d #_ #k0 #H destruct
-| #G #L #V #T #U #d #_ #k0 #H destruct
-| #G #L #W #T #U #d #_ #k0 #H destruct
+[ #G #L #d #s #s0 #H destruct //
+| #G #L #K #V #W #U #i #d #_ #_ #_ #s0 #H destruct
+| #G #L #K #W #V #i #_ #_ #s0 #H destruct
+| #G #L #K #W #V #U #i #d #_ #_ #_ #s0 #H destruct
+| #a #I #G #L #V #T #U #d #_ #s0 #H destruct
+| #G #L #V #T #U #d #_ #s0 #H destruct
+| #G #L #W #T #U #d #_ #s0 #H destruct
 qed-.
 
 (* Basic_1: was just: sty0_gen_sort *)
-lemma lstas_inv_sort1: ∀h,G,L,X,k,d. ⦃G, L⦄ ⊢ ⋆k •*[h, d] X → X = ⋆((next h)^d k).
+lemma lstas_inv_sort1: ∀h,G,L,X,s,d. ⦃G, L⦄ ⊢ ⋆s •*[h, d] X → X = ⋆((next h)^d s).
 /2 width=5 by lstas_inv_sort1_aux/
 qed-.
 
@@ -67,7 +67,7 @@ fact lstas_inv_lref1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀j
                                        ⬆[0, j+1] V ≡ U & d = d0+1
                           ).
 #h #G #L #T #U #d * -G -L -T -U -d
-[ #G #L #d #k #j #H destruct
+[ #G #L #d #s #j #H destruct
 | #G #L #K #V #W #U #i #d #HLK #HVW #HWU #j #H destruct /3 width=6 by or3_intro0, ex3_3_intro/
 | #G #L #K #W #V #i #HLK #HWV #j #H destruct /3 width=5 by or3_intro1, ex4_3_intro/
 | #G #L #K #W #V #U #i #d #HLK #HWV #HWU #j #H destruct /3 width=8 by or3_intro2, ex4_4_intro/ 
@@ -115,7 +115,7 @@ qed-.
 
 fact lstas_inv_gref1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀p0. T = §p0 → ⊥.
 #h #G #L #T #U #d * -G -L -T -U -d
-[ #G #L #d #k #p0 #H destruct
+[ #G #L #d #s #p0 #H destruct
 | #G #L #K #V #W #U #i #d #_ #_ #_ #p0 #H destruct
 | #G #L #K #W #V #i #_ #_ #p0 #H destruct
 | #G #L #K #W #V #U #i #d #_ #_ #_ #p0 #H destruct
@@ -131,7 +131,7 @@ qed-.
 fact lstas_inv_bind1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀b,J,X,Y. T = ⓑ{b,J}Y.X →
                           ∃∃Z. ⦃G, L.ⓑ{J}Y⦄ ⊢ X •*[h, d] Z & U = ⓑ{b,J}Y.Z.
 #h #G #L #T #U #d * -G -L -T -U -d
-[ #G #L #d #k #b #J #X #Y #H destruct
+[ #G #L #d #s #b #J #X #Y #H destruct
 | #G #L #K #V #W #U #i #d #_ #_ #_ #b #J #X #Y #H destruct
 | #G #L #K #W #V #i #_ #_ #b #J #X #Y #H destruct
 | #G #L #K #W #V #U #i #d #_ #_ #_ #b #J #X #Y #H destruct
@@ -150,7 +150,7 @@ qed-.
 fact lstas_inv_appl1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀X,Y. T = ⓐY.X →
                           ∃∃Z. ⦃G, L⦄ ⊢ X •*[h, d] Z & U = ⓐY.Z.
 #h #G #L #T #U #d * -G -L -T -U -d
-[ #G #L #d #k #X #Y #H destruct
+[ #G #L #d #s #X #Y #H destruct
 | #G #L #K #V #W #U #i #d #_ #_ #_ #X #Y #H destruct
 | #G #L #K #W #V #i #_ #_ #X #Y #H destruct
 | #G #L #K #W #V #U #i #d #_ #_ #_ #X #Y #H destruct
@@ -169,7 +169,7 @@ qed-.
 fact lstas_inv_cast1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀X,Y. T = ⓝY.X →
                           ⦃G, L⦄ ⊢ X •*[h, d] U.
 #h #G #L #T #U #d * -G -L -T -U -d
-[ #G #L #d #k #X #Y #H destruct
+[ #G #L #d #s #X #Y #H destruct
 | #G #L #K #V #W #U #i #d #_ #_ #_ #X #Y #H destruct
 | #G #L #K #W #V #i #_ #_ #X #Y #H destruct
 | #G #L #K #W #V #U #i #d #_ #_ #_ #X #Y #H destruct