partial commit: "static" component ....

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / ssta_aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
index 0f035cf7ca2018a5b4a579b53f71e3ecdc76bf50..27c12c465fbdf1629a3e212017f398198aa0b5b9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma
@@ -19,22 +19,22 @@ include "basic_2/static/ssta.ma".
 
 (* Properties on atomic arity assignment for terms **************************)
 
-lemma ssta_aaa: ∀h,g,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ⦃G, L⦄ ⊢ U ⁝ A.
-#h #g #L #T #A #H elim H -L -T -A
-[ #L #k #U #l #H
+lemma ssta_aaa: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ⦃G, L⦄ ⊢ U ⁝ A.
+#h #g #G #L #T #A #H elim H -G -L -T -A
+[ #G #L #k #U #l #H
   elim (ssta_inv_sort1 … H) -H #_ #H destruct //
-| #I #L #K #V #B #i #HLK #HV #IHV #U #l #H
+| #I #G #L #K #V #B #i #HLK #HV #IHV #U #l #H
   elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0 ] #HLK0 #HVW0 #HU [ #H ]
   lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct
   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
   @(aaa_lift … HLK … HU) -HU -L // -HV /2 width=2/
-| #a #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
+| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
   elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/
-| #a #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
+| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
   elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/
-| #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
+| #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
   elim (ssta_inv_appl1 … H) -H #U #HTU #H destruct /3 width=3/
-| #L #V #T #A #_ #_ #IHV #IHT #X #l #H
+| #G #L #V #T #A #_ #_ #IHV #IHT #X #l #H
   lapply (ssta_inv_cast1 … H) -H /2 width=2/
 ]
 qed.