From 3cf712a7a75b57fb24f8dbed3f6f28d70dbf5be3 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 1 Aug 2013 15:05:48 +0000
Subject: [PATCH] partial commit: "static" component ....

---
 .../{atomicarity_3.ma => atomicarity_4.ma}    |   4 +-
 .../{lrsubeqa_2.ma => lrsubeqa_3.ma}          |   4 +-
 .../{statictype_6.ma => statictype_7.ma}      |   4 +-
 .../lambdadelta/basic_2/static/aaa.ma         | 212 +++++++++---------
 .../lambdadelta/basic_2/static/aaa_aaa.ma     |  16 +-
 .../lambdadelta/basic_2/static/aaa_lift.ma    |  36 +--
 .../lambdadelta/basic_2/static/aaa_lifts.ma   |   6 +-
 .../lambdadelta/basic_2/static/lsuba.ma       |  72 +++---
 .../lambdadelta/basic_2/static/lsuba_aaa.ma   |  14 +-
 .../lambdadelta/basic_2/static/lsuba_ldrop.ma |  12 +-
 .../lambdadelta/basic_2/static/lsuba_lsuba.ma |   4 +-
 .../lambdadelta/basic_2/static/ssta.ma        | 180 +++++++--------
 .../lambdadelta/basic_2/static/ssta_aaa.ma    |  16 +-
 .../lambdadelta/basic_2/static/ssta_lift.ma   |  54 ++---
 .../lambdadelta/basic_2/static/ssta_ssta.ma   |  20 +-
 15 files changed, 330 insertions(+), 324 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{atomicarity_3.ma => atomicarity_4.ma} (89%)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lrsubeqa_2.ma => lrsubeqa_3.ma} (91%)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{statictype_6.ma => statictype_7.ma} (84%)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.ma
similarity index 89%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_3.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.ma
index 42f9d584d..e6a1b0924 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/atomicarity_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃G, L⦄ ⊢ break term 46 T ⁝ break term 46 A )"
+notation "hvbox( ⦃term 46 G, break term 46 L⦄ ⊢ break term 46 T ⁝ break term 46 A )"
    non associative with precedence 45
-   for @{ 'AtomicArity $L $T $A }.
+   for @{ 'AtomicArity $G $L $T $A }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma
similarity index 91%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_2.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma
index c45cdebdc..e46553827 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_2.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⁝ ⊑ break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEqA $T1 $T2 }.
+   for @{ 'LRSubEqA $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_7.ma
similarity index 84%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_6.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_7.ma
index c389e2d17..822d8888c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_7.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 g ] break ⦃ term 46 l , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 h, break term 46 g ] break ⦃ term 46 l , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'StaticType $h $g $L $T1 $T2 $l }.
+   for @{ 'StaticType $h $g $G $L $T1 $T2 $l }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
index 4c4f1e572..cc1ed23c2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
@@ -12,132 +12,134 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/atomicarity_3.ma".
+include "basic_2/notation/relations/atomicarity_4.ma".
 include "basic_2/grammar/aarity.ma".
+include "basic_2/grammar/genv.ma".
 include "basic_2/relocation/ldrop.ma".
 
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
 
-inductive aaa: lenv → term → predicate aarity ≝
-| aaa_sort: ∀L,k. aaa L (⋆k) (⓪)
-| aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
-| aaa_abbr: ∀a,L,V,T,B,A.
-            aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓ{a}V. T) A
-| aaa_abst: ∀a,L,V,T,B,A.
-            aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛ{a}V. T) (②B. A)
-| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (②B. A) → aaa L (ⓐV. T) A
-| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (ⓝV. T) A
+(* activate genv *)
+inductive aaa: relation4 genv lenv term aarity ≝
+| aaa_sort: ∀G,L,k. aaa G L (⋆k) (⓪)
+| aaa_lref: ∀I,G,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I}V → aaa G K V B → aaa G L (#i) B
+| aaa_abbr: ∀a,G,L,V,T,B,A.
+            aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{a}V.T) A
+| aaa_abst: ∀a,G,L,V,T,B,A.
+            aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ{a}V.T) (②B.A)
+| aaa_appl: ∀G,L,V,T,B,A. aaa G L V B → aaa G L T (②B.A) → aaa G L (ⓐV.T) A
+| aaa_cast: ∀G,L,V,T,A. aaa G L V A → aaa G L T A → aaa G L (ⓝV.T) A
 .
 
 interpretation "atomic arity assignment (term)"
-   'AtomicArity L T A = (aaa L T A).
+   'AtomicArity G L T A = (aaa G L T A).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact aaa_inv_sort_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀k. T = ⋆k → A = ⓪.
-#L #T #A * -L -T -A
+fact aaa_inv_sort_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀k. T = ⋆k → A = ⓪.
+#G #L #T #A * -G -L -T -A
 [ //
-| #I #L #K #V #B #i #_ #_ #k #H destruct
-| #a #L #V #T #B #A #_ #_ #k #H destruct
-| #a #L #V #T #B #A #_ #_ #k #H destruct
-| #L #V #T #B #A #_ #_ #k #H destruct
-| #L #V #T #A #_ #_ #k #H destruct
+| #I #G #L #K #V #B #i #_ #_ #k #H destruct
+| #a #G #L #V #T #B #A #_ #_ #k #H destruct
+| #a #G #L #V #T #B #A #_ #_ #k #H destruct
+| #G #L #V #T #B #A #_ #_ #k #H destruct
+| #G #L #V #T #A #_ #_ #k #H destruct
 ]
-qed.
-
-lemma aaa_inv_sort: ∀L,A,k. ⦃G, L⦄ ⊢ ⋆k ⁝ A → A = ⓪.
-/2 width=5/ qed-.
-
-fact aaa_inv_lref_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #i →
-                       ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A.
-#L #T #A * -L -T -A
-[ #L #k #i #H destruct
-| #I #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/
-| #a #L #V #T #B #A #_ #_ #i #H destruct
-| #a #L #V #T #B #A #_ #_ #i #H destruct
-| #L #V #T #B #A #_ #_ #i #H destruct
-| #L #V #T #A #_ #_ #i #H destruct
+qed-.
+
+lemma aaa_inv_sort: ∀G,L,A,k. ⦃G, L⦄ ⊢ ⋆k ⁝ A → A = ⓪.
+/2 width=6 by aaa_inv_sort_aux/ qed-.
+
+fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #i →
+                       ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #i #H destruct
+| #I #G #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/
+| #a #G #L #V #T #B #A #_ #_ #i #H destruct
+| #a #G #L #V #T #B #A #_ #_ #i #H destruct
+| #G #L #V #T #B #A #_ #_ #i #H destruct
+| #G #L #V #T #A #_ #_ #i #H destruct
 ]
-qed.
-
-lemma aaa_inv_lref: ∀L,A,i. ⦃G, L⦄ ⊢ #i ⁝ A →
-                    ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A.
-/2 width=3/ qed-.
-
-fact aaa_inv_gref_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p. T = §p → ⊥.
-#L #T #A * -L -T -A
-[ #L #k #q #H destruct
-| #I #L #K #V #B #i #HLK #HB #q #H destruct
-| #a #L #V #T #B #A #_ #_ #q #H destruct
-| #a #L #V #T #B #A #_ #_ #q #H destruct
-| #L #V #T #B #A #_ #_ #q #H destruct
-| #L #V #T #A #_ #_ #q #H destruct
+qed-.
+
+lemma aaa_inv_lref: ∀G,L,A,i. ⦃G, L⦄ ⊢ #i ⁝ A →
+                    ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+/2 width=3 by aaa_inv_lref_aux/ qed-.
+
+fact aaa_inv_gref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p. T = §p → ⊥.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #q #H destruct
+| #I #G #L #K #V #B #i #HLK #HB #q #H destruct
+| #a #G #L #V #T #B #A #_ #_ #q #H destruct
+| #a #G #L #V #T #B #A #_ #_ #q #H destruct
+| #G #L #V #T #B #A #_ #_ #q #H destruct
+| #G #L #V #T #A #_ #_ #q #H destruct
 ]
-qed.
-
-lemma aaa_inv_gref: ∀L,A,p. ⦃G, L⦄ ⊢ §p ⁝ A → ⊥.
-/2 width=6/ qed-.
-
-fact aaa_inv_abbr_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U →
-                       ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & L. ⓓW ⊢ U ⁝ A.
-#L #T #A * -L -T -A
-[ #L #k #a #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #a #W #U #H destruct
-| #b #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=2/
-| #b #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #L #V #T #A #_ #_ #a #W #U #H destruct
+qed-.
+
+lemma aaa_inv_gref: ∀G,L,A,p. ⦃G, L⦄ ⊢ §p ⁝ A → ⊥.
+/2 width=7 by aaa_inv_gref_aux/ qed-.
+
+fact aaa_inv_abbr_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U →
+                       ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L.ⓓW⦄ ⊢ U ⁝ A.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #a #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
+| #b #G #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=2/
+| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #G #L #V #T #A #_ #_ #a #W #U #H destruct
 ]
-qed.
-
-lemma aaa_inv_abbr: ∀a,L,V,T,A. ⦃G, L⦄ ⊢ ⓓ{a}V. T ⁝ A →
-                    ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & L. ⓓV ⊢ T ⁝ A.
-/2 width=4/ qed-.
-
-fact aaa_inv_abst_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓛ{a}W. U →
-                       ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & L. ⓛW ⊢ U ⁝ B2 & A = ②B1. B2.
-#L #T #A * -L -T -A
-[ #L #k #a #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #a #W #U #H destruct
-| #b #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #b #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=5/
-| #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #L #V #T #A #_ #_ #a #W #U #H destruct
+qed-.
+
+lemma aaa_inv_abbr: ∀a,G,L,V,T,A. ⦃G, L⦄ ⊢ ⓓ{a}V. T ⁝ A →
+                    ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L.ⓓV⦄ ⊢ T ⁝ A.
+/2 width=4 by aaa_inv_abbr_aux/ qed-.
+
+fact aaa_inv_abst_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓛ{a}W. U →
+                       ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & ⦃G, L.ⓛW⦄ ⊢ U ⁝ B2 & A = ②B1.B2.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #a #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
+| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #b #G #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=5/
+| #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #G #L #V #T #A #_ #_ #a #W #U #H destruct
 ]
-qed.
-
-lemma aaa_inv_abst: ∀a,L,W,T,A. ⦃G, L⦄ ⊢ ⓛ{a}W. T ⁝ A →
-                    ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & L. ⓛW ⊢ T ⁝ B2 & A = ②B1. B2.
-/2 width=4/ qed-.
-
-fact aaa_inv_appl_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓐW. U →
-                       ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L⦄ ⊢ U ⁝ ②B. A.
-#L #T #A * -L -T -A
-[ #L #k #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3/
-| #L #V #T #A #_ #_ #W #U #H destruct
+qed-.
+
+lemma aaa_inv_abst: ∀a,G,L,W,T,A. ⦃G, L⦄ ⊢ ⓛ{a}W. T ⁝ A →
+                    ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & ⦃G, L.ⓛW⦄ ⊢ T ⁝ B2 & A = ②B1.B2.
+/2 width=4 by aaa_inv_abst_aux/ qed-.
+
+fact aaa_inv_appl_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
+                       ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L⦄ ⊢ U ⁝ ②B.A.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #G #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3/
+| #G #L #V #T #A #_ #_ #W #U #H destruct
 ]
-qed.
+qed-.
 
-lemma aaa_inv_appl: ∀L,V,T,A. ⦃G, L⦄ ⊢ ⓐV. T ⁝ A →
-                    ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L⦄ ⊢ T ⁝ ②B. A.
-/2 width=3/ qed-.
+lemma aaa_inv_appl: ∀G,L,V,T,A. ⦃G, L⦄ ⊢ ⓐV.T ⁝ A →
+                    ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L⦄ ⊢ T ⁝ ②B.A.
+/2 width=3 by aaa_inv_appl_aux/ qed-.
 
-fact aaa_inv_cast_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓝW. U →
+fact aaa_inv_cast_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓝW. U →
                        ⦃G, L⦄ ⊢ W ⁝ A ∧ ⦃G, L⦄ ⊢ U ⁝ A.
-#L #T #A * -L -T -A
-[ #L #k #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #A #HV #HT #W #U #H destruct /2 width=1/
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #G #L #V #T #A #HV #HT #W #U #H destruct /2 width=1/
 ]
-qed.
+qed-.
 
-lemma aaa_inv_cast: ∀L,W,T,A. ⦃G, L⦄ ⊢ ⓝW. T ⁝ A →
+lemma aaa_inv_cast: ∀G,L,W,T,A. ⦃G, L⦄ ⊢ ⓝW. T ⁝ A →
                     ⦃G, L⦄ ⊢ W ⁝ A ∧ ⦃G, L⦄ ⊢ T ⁝ A.
-/2 width=3/ qed-.
+/2 width=3 by aaa_inv_cast_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
index 4bf7888c0..d0cff387f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
@@ -19,21 +19,21 @@ include "basic_2/static/aaa.ma".
 
 (* Main properties **********************************************************)
 
-theorem aaa_mono: ∀L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
-#L #T #A1 #H elim H -L -T -A1
-[ #L #k #A2 #H
+theorem aaa_mono: ∀G,L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
+#G #L #T #A1 #H elim H -G -L -T -A1
+[ #G #L #k #A2 #H
   >(aaa_inv_sort … H) -H //
-| #I1 #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
+| #I1 #G #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
   elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2
   lapply (ldrop_mono … HLK1 … HLK2) -L #H destruct /2 width=1/
-| #a #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
+| #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
   elim (aaa_inv_abbr … H) -H /2 width=1/
-| #a #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
+| #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
   elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1/
-| #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
+| #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
   elim (aaa_inv_appl … H) -H #B2 #_ #HA2
   lapply (IHA1 … HA2) -L #H destruct //
-| #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
+| #G #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
   elim (aaa_inv_cast … H) -H /2 width=1/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
index 992c8139c..ba7d02b91 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
@@ -19,53 +19,53 @@ include "basic_2/static/aaa.ma".
 
 (* Properties concerning basic relocation ***********************************)
 
-lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
-                ∀T2. ⇧[d, e] T1 ≡ T2 → L2 ⊢ T2 ⁝ A.
-#L1 #T1 #A #H elim H -L1 -T1 -A
-[ #L1 #k #L2 #d #e #_ #T2 #H
+lemma aaa_lift: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+                ∀T2. ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+#G #L1 #T1 #A #H elim H -G -L1 -T1 -A
+[ #G #L1 #k #L2 #d #e #_ #T2 #H
   >(lift_inv_sort1 … H) -H //
-| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
   elim (lift_inv_lref1 … H) -H * #Hid #H destruct
   [ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
     elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
     /3 width=8/
   | lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
   ]
-| #a #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
   elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
   /4 width=4/
-| #a #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
   elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
   /4 width=4/
-| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+| #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
   elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
   /3 width=4/
-| #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H
+| #G #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H
   elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
   /3 width=4/
 ]
 qed.
 
-lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
-                    ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ⁝ A.
-#L2 #T2 #A #H elim H -L2 -T2 -A
-[ #L2 #k #L1 #d #e #_ #T1 #H
+lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+                    ∀T1. ⇧[d, e] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
+#G #L2 #T2 #A #H elim H -G -L2 -T2 -A
+[ #G #L2 #k #L1 #d #e #_ #T1 #H
   >(lift_inv_sort2 … H) -H //
-| #I #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H
+| #I #G #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
   [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/
   | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/
   ]
-| #a #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
   /4 width=4/
-| #a #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
   /4 width=4/
-| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+| #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
   /3 width=4/
-| #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H
+| #G #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
   /3 width=4/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
index 7afcc4131..6cd3855c5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lifts.ma
@@ -19,9 +19,9 @@ include "basic_2/static/aaa_lift.ma".
 
 (* Properties concerning generic relocation *********************************)
 
-lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →
-                                  L1 ⊢ T1 ⁝ A →  L2 ⊢ T2 ⁝ A.
-#L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des
+lemma aaa_lifts: ∀G,L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →
+                 ⦃G, L1⦄ ⊢ T1 ⁝ A → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+#G #L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des
 [ #L #T1 #H #HT1
   <(lifts_inv_nil … H) -H //
 | #L1 #L #L2 #des #d #e #_ #HL2 #IHL1 #T1 #H #HT1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
index f3e13c105..c6d4478de 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
@@ -12,89 +12,89 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/lrsubeqa_2.ma".
+include "basic_2/notation/relations/lrsubeqa_3.ma".
+include "basic_2/static/aaa.ma". (**) (* disambiguation error *)
 include "basic_2/substitution/lsubr.ma".
-include "basic_2/static/aaa.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
 
-inductive lsuba: relation lenv ≝
-| lsuba_atom: lsuba (⋆) (⋆)
-| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsuba_abbr: ∀L1,L2,W,V,A. L1 ⊢ ⓝW.V ⁝ A → L2 ⊢ W ⁝ A →
-              lsuba L1 L2 → lsuba (L1.ⓓⓝW.V) (L2.ⓛW)
+inductive lsuba (G:genv): relation lenv ≝
+| lsuba_atom: lsuba G (⋆) (⋆)
+| lsuba_pair: ∀I,L1,L2,V. lsuba G L1 L2 → lsuba G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsuba_abbr: ∀L1,L2,W,V,A. ⦃G, L1⦄ ⊢ ⓝW.V ⁝ A → ⦃G, L2⦄ ⊢ W ⁝ A →
+              lsuba G L1 L2 → lsuba G (L1.ⓓⓝW.V) (L2.ⓛW)
 .
 
 interpretation
   "local environment refinement (atomic arity assigment)"
-  'LRSubEqA L1 L2 = (lsuba L1 L2).
+  'LRSubEqA G L1 L2 = (lsuba G L1 L2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ⁝⊑ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_atom1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #V #_ #H destruct
 | #L1 #L2 #W #V #A #_ #_ #_ #H destruct
 ]
 qed-.
 
-lemma lsuba_inv_atom1: ∀L2. ⋆ ⁝⊑ L2 → L2 = ⋆.
-/2 width=3 by lsuba_inv_atom1_aux/ qed-.
+lemma lsuba_inv_atom1: ∀G,L2. G ⊢ ⋆ ⁝⊑ L2 → L2 = ⋆.
+/2 width=4 by lsuba_inv_atom1_aux/ qed-.
 
-fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
-                          (∃∃K2. K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
-                          ∃∃K2,W,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
-                                      I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_pair1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+                          (∃∃K2. G ⊢ K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
+                          ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                      G ⊢ K1 ⁝⊑ K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+#G #L1 #L2 * -L1 -L2
 [ #J #K1 #X #H destruct
 | #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
 | #L1 #L2 #W #V #A #HV #HW #HL12 #J #K1 #X #H destruct /3 width=9/
 ]
 qed-.
 
-lemma lsuba_inv_pair1: ∀I,K1,L2,X. K1.ⓑ{I}X ⁝⊑ L2 →
-                       (∃∃K2. K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
-                       ∃∃K2,W,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+lemma lsuba_inv_pair1: ∀I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⁝⊑ L2 →
+                       (∃∃K2. G ⊢ K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
+                       ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⁝⊑ K2 &
                                    I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
 /2 width=3 by lsuba_inv_pair1_aux/ qed-.
 
-fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ⁝⊑ L2 → L2 = ⋆ → L1 = ⋆.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → L2 = ⋆ → L1 = ⋆.
+#G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #V #_ #H destruct
 | #L1 #L2 #W #V #A #_ #_ #_ #H destruct
 ]
 qed-.
 
-lemma lsubc_inv_atom2: ∀L1. L1 ⁝⊑ ⋆ → L1 = ⋆.
-/2 width=3 by lsuba_inv_atom2_aux/ qed-.
+lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⁝⊑ ⋆ → L1 = ⋆.
+/2 width=4 by lsuba_inv_atom2_aux/ qed-.
 
-fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
-                          (∃∃K1. K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
-                          ∃∃K1,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
-                                    I = Abst & L1 = K1.ⓓⓝW.V.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
+                          (∃∃K1. G ⊢ K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
+                          ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                    G ⊢ K1 ⁝⊑ K2 & I = Abst & L1 = K1.ⓓⓝW.V.
+#G #L1 #L2 * -L1 -L2
 [ #J #K2 #U #H destruct
 | #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3/
 | #L1 #L2 #W #V #A #HV #HW #HL12 #J #K2 #U #H destruct /3 width=7/
 ]
 qed-.
 
-lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ⁝⊑ K2.ⓑ{I}W →
-                       (∃∃K1. K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
-                       ∃∃K1,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+lemma lsuba_inv_pair2: ∀I,G,L1,K2,W. G ⊢ L1 ⁝⊑ K2.ⓑ{I}W →
+                       (∃∃K1. G ⊢ K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
+                       ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⁝⊑ K2 &
                                  I = Abst & L1 = K1.ⓓⓝW.V.
 /2 width=3 by lsuba_inv_pair2_aux/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lsuba_fwd_lsubr: ∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑ L2.
-#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → L1 ⊑ L2.
+#G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lsuba_refl: ∀L. L ⁝⊑ L.
-#L elim L -L // /2 width=1/
+lemma lsuba_refl: ∀G,L. G ⊢ L ⁝⊑ L.
+#G #L elim L -L // /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma
index 8539db3db..8818ae48c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma
@@ -19,10 +19,11 @@ include "basic_2/static/lsuba_ldrop.ma".
 
 (* Properties concerning atomic arity assignment ****************************)
 
-lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ⁝ A → ∀L2. L1 ⁝⊑ L2 → L2 ⊢ V ⁝ A.
-#L1 #V #A #H elim H -L1 -V -A
+lemma lsuba_aaa_conf: ∀G,L1,V,A. ⦃G, L1⦄ ⊢ V ⁝ A →
+                      ∀L2. G ⊢ L1 ⁝⊑ L2 → ⦃G, L2⦄ ⊢ V ⁝ A.
+#G #L1 #V #A #H elim H -G -L1 -V -A
 [ //
-| #I #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12
+| #I #G #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12
   elim (lsuba_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
   elim (lsuba_inv_pair1 … H) -H * #K2
   [ #HK12 #H destruct /3 width=5/
@@ -36,10 +37,11 @@ lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ⁝ A → ∀L2. L1 ⁝⊑ L2 → L2 
 ]
 qed-.
 
-lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ⁝ A → ∀L1. L1 ⁝⊑ L2 → L1 ⊢ V ⁝ A.
-#L2 #V #A #H elim H -L2 -V -A
+lemma lsuba_aaa_trans: ∀G,L2,V,A. ⦃G, L2⦄ ⊢ V ⁝ A →
+                       ∀L1. G ⊢ L1 ⁝⊑ L2 → ⦃G, L1⦄ ⊢ V ⁝ A.
+#G #L2 #V #A #H elim H -G -L2 -V -A
 [ //
-| #I #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12
+| #I #G #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12
   elim (lsuba_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
   elim (lsuba_inv_pair2 … H) -H * #K1
   [ #HK12 #H destruct /3 width=5/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma
index 863ad74d7..bb412f1c5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma
@@ -19,9 +19,9 @@ include "basic_2/static/lsuba.ma".
 (* Properties concerning basic local environment slicing ********************)
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
-                           ∃∃K2. K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
-#L1 #L2 #H elim H -L1 -L2
+lemma lsuba_ldrop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+                           ∃∃K2. G ⊢ K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
+#G #L1 #L2 #H elim H -L1 -L2
 [ /2 width=3/
 | #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
   elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1
@@ -41,9 +41,9 @@ lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡
 qed-.
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                            ∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
-#L1 #L2 #H elim H -L1 -L2
+lemma lsuba_ldrop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+                            ∃∃K1. G ⊢ K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
+#G #L1 #L2 #H elim H -L1 -L2
 [ /2 width=3/
 | #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
   elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma
index 2738570ab..eb7ae1386 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma
@@ -18,8 +18,8 @@ include "basic_2/static/lsuba_aaa.ma".
 
 (* Main properties **********************************************************)
 
-theorem lsuba_trans: ∀L1,L. L1 ⁝⊑ L → ∀L2. L ⁝⊑ L2 → L1 ⁝⊑ L2.
-#L1 #L #H elim H -L1 -L
+theorem lsuba_trans: ∀G,L1,L. G ⊢ L1 ⁝⊑ L → ∀L2. G ⊢ L ⁝⊑ L2 → G ⊢ L1 ⁝⊑ L2.
+#G #L1 #L #H elim H -L1 -L
 [ #X #H >(lsuba_inv_atom1 … H) -H //
 | #I #L1 #L #Y #HL1 #IHL1 #X #H
   elim (lsuba_inv_pair1 … H) -H * #L2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
index 9421d7436..ac9033c53 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma
@@ -12,137 +12,139 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/statictype_6.ma".
+include "basic_2/notation/relations/statictype_7.ma".
+include "basic_2/grammar/genv.ma". (**) (* disambiguation error *)
 include "basic_2/relocation/ldrop.ma".
 include "basic_2/static/sd.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
 
-inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝
-| ssta_sort: ∀L,k,l. deg h g k l → ssta h g l L (⋆k) (⋆(next h k))
-| ssta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l K V W →
-             ⇧[0, i + 1] W ≡ U → ssta h g l L (#i) U
-| ssta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l K W V →
-             ⇧[0, i + 1] W ≡ U → ssta h g (l+1) L (#i) U
-| ssta_bind: ∀a,I,L,V,T,U,l. ssta h g l (L. ⓑ{I} V) T U →
-             ssta h g l L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
-| ssta_appl: ∀L,V,T,U,l. ssta h g l L T U →
-             ssta h g l L (ⓐV.T) (ⓐV.U)
-| ssta_cast: ∀L,W,T,U,l. ssta h g l L T U → ssta h g l L (ⓝW. T) U
+(* activate genv *)
+inductive ssta (h:sh) (g:sd h): nat → genv → lenv → relation term ≝
+| ssta_sort: ∀G,L,k,l. deg h g k l → ssta h g l G L (⋆k) (⋆(next h k))
+| ssta_ldef: ∀G,L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l G K V W →
+             ⇧[0, i + 1] W ≡ U → ssta h g l G L (#i) U
+| ssta_ldec: ∀G,L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l G K W V →
+             ⇧[0, i + 1] W ≡ U → ssta h g (l+1) G L (#i) U
+| ssta_bind: ∀a,I,G,L,V,T,U,l. ssta h g l G (L. ⓑ{I} V) T U →
+             ssta h g l G L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
+| ssta_appl: ∀G,L,V,T,U,l. ssta h g l G L T U →
+             ssta h g l G L (ⓐV.T) (ⓐV.U)
+| ssta_cast: ∀G,L,W,T,U,l. ssta h g l G L T U → ssta h g l G L (ⓝW.T) U
 .
 
 interpretation "stratified static type assignment (term)"
-   'StaticType h g L T U l = (ssta h g l L T U).
+   'StaticType h g G L T U l = (ssta h g l G L T U).
 
-definition ssta_step: ∀h. sd h → lenv → relation term ≝ λh,g,L,T,U.
+definition ssta_step: ∀h. sd h → genv → lenv → relation term ≝ λh,g,G,L,T,U.
                       ∃l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄.
 
 (* Basic inversion lemmas ************************************************)
 
-fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀k0. T = ⋆k0 →
+fact ssta_inv_sort1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀k0. T = ⋆k0 →
                          deg h g k0 l ∧ U = ⋆(next h k0).
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #Hkl #k0 #H destruct /2 width=1/
-| #L #K #V #W #U #i #l #_ #_ #_ #k0 #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #k0 #H destruct
-| #a #I #L #V #T #U #l #_ #k0 #H destruct
-| #L #V #T #U #l #_ #k0 #H destruct
-| #L #W #T #U #l #_ #k0 #H destruct
-qed.
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #Hkl #k0 #H destruct /2 width=1/
+| #G #L #K #V #W #U #i #l #_ #_ #_ #k0 #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #k0 #H destruct
+| #a #I #G #L #V #T #U #l #_ #k0 #H destruct
+| #G #L #V #T #U #l #_ #k0 #H destruct
+| #G #L #W #T #U #l #_ #k0 #H destruct
+qed-.
 
 (* Basic_1: was just: sty0_gen_sort *)
-lemma ssta_inv_sort1: ∀h,g,L,U,k,l. ⦃G, L⦄ ⊢ ⋆k •[h, g] ⦃l, U⦄ →
+lemma ssta_inv_sort1: ∀h,g,G,L,U,k,l. ⦃G, L⦄ ⊢ ⋆k •[h, g] ⦃l, U⦄ →
                       deg h g k l ∧ U = ⋆(next h k).
-/2 width=4/ qed-.
+/2 width=5 by ssta_inv_sort1_aux/ qed-.
 
-fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀j. T = #j →
-                         (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
+fact ssta_inv_lref1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀j. T = #j →
+                         (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
                                    ⇧[0, j + 1] W ≡ U
                          ) ∨
-                         (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
+                         (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃G, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
                                       ⇧[0, j + 1] W ≡ U & l = l0 + 1
                          ).
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #j #H destruct
-| #L #K #V #W #U #i #l #HLK #HVW #HWU #j #H destruct /3 width=6/
-| #L #K #W #V #U #i #l #HLK #HWV #HWU #j #H destruct /3 width=8/
-| #a #I #L #V #T #U #l #_ #j #H destruct
-| #L #V #T #U #l #_ #j #H destruct
-| #L #W #T #U #l #_ #j #H destruct
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #j #H destruct
+| #G #L #K #V #W #U #i #l #HLK #HVW #HWU #j #H destruct /3 width=6/
+| #G #L #K #W #V #U #i #l #HLK #HWV #HWU #j #H destruct /3 width=8/
+| #a #I #G #L #V #T #U #l #_ #j #H destruct
+| #G #L #V #T #U #l #_ #j #H destruct
+| #G #L #W #T #U #l #_ #j #H destruct
 ]
-qed.
+qed-.
 
 (* Basic_1: was just: sty0_gen_lref *)
-lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃G, L⦄ ⊢ #i •[h, g] ⦃l, U⦄ →
-                      (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
+lemma ssta_inv_lref1: ∀h,g,G,L,U,i,l. ⦃G, L⦄ ⊢ #i •[h, g] ⦃l, U⦄ →
+                      (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
                                 ⇧[0, i + 1] W ≡ U
                       ) ∨
-                      (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
+                      (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃G, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
                                    ⇧[0, i + 1] W ≡ U & l = l0 + 1
                       ).
-/2 width=3/ qed-.
-
-fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #p0 #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct
-| #a #I #L #V #T #U #l #_ #p0 #H destruct
-| #L #V #T #U #l #_ #p0 #H destruct
-| #L #W #T #U #l #_ #p0 #H destruct
-qed.
-
-lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃G, L⦄ ⊢ §p •[h, g] ⦃l, U⦄ → ⊥.
-/2 width=9/ qed-.
-
-fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
+/2 width=3 by ssta_inv_lref1_aux/ qed-.
+
+fact ssta_inv_gref1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥.
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #p0 #H destruct
+| #G #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct
+| #a #I #G #L #V #T #U #l #_ #p0 #H destruct
+| #G #L #V #T #U #l #_ #p0 #H destruct
+| #G #L #W #T #U #l #_ #p0 #H destruct
+qed-.
+
+lemma ssta_inv_gref1: ∀h,g,G,L,U,p,l. ⦃G, L⦄ ⊢ §p •[h, g] ⦃l, U⦄ → ⊥.
+/2 width=10 by ssta_inv_gref1_aux/ qed-.
+
+fact ssta_inv_bind1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
                          ∀a,I,X,Y. T = ⓑ{a,I}Y.X →
-                         ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #a #I #X #Y #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
-| #b #J #L #V #T #U #l #HTU #a #I #X #Y #H destruct /2 width=3/
-| #L #V #T #U #l #_ #a #I #X #Y #H destruct
-| #L #W #T #U #l #_ #a #I #X #Y #H destruct
+                         ∃∃Z. ⦃G, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #a #I #X #Y #H destruct
+| #G #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
+| #b #J #G #L #V #T #U #l #HTU #a #I #X #Y #H destruct /2 width=3/
+| #G #L #V #T #U #l #_ #a #I #X #Y #H destruct
+| #G #L #W #T #U #l #_ #a #I #X #Y #H destruct
 ]
-qed.
+qed-.
 
 (* Basic_1: was just: sty0_gen_bind *)
-lemma ssta_inv_bind1: ∀h,g,a,I,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓑ{a,I}Y.X •[h, g] ⦃l, U⦄ →
-                      ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
-/2 width=3/ qed-.
+lemma ssta_inv_bind1: ∀h,g,a,I,G,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓑ{a,I}Y.X •[h, g] ⦃l, U⦄ →
+                      ∃∃Z. ⦃G, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
+/2 width=3 by ssta_inv_bind1_aux/ qed-.
 
-fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀X,Y. T = ⓐY.X →
+fact ssta_inv_appl1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀X,Y. T = ⓐY.X →
                          ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓐY.Z.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #X #Y #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #X #Y #H destruct
-| #a #I #L #V #T #U #l #_ #X #Y #H destruct
-| #L #V #T #U #l #HTU #X #Y #H destruct /2 width=3/
-| #L #W #T #U #l #_ #X #Y #H destruct
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #X #Y #H destruct
+| #G #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #X #Y #H destruct
+| #a #I #G #L #V #T #U #l #_ #X #Y #H destruct
+| #G #L #V #T #U #l #HTU #X #Y #H destruct /2 width=3/
+| #G #L #W #T #U #l #_ #X #Y #H destruct
 ]
-qed.
+qed-.
 
 (* Basic_1: was just: sty0_gen_appl *)
-lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓐY.X •[h, g] ⦃l, U⦄ →
+lemma ssta_inv_appl1: ∀h,g,G,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓐY.X •[h, g] ⦃l, U⦄ →
                       ∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓐY.Z.
-/2 width=3/ qed-.
+/2 width=3 by ssta_inv_appl1_aux/ qed-.
 
-fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
+fact ssta_inv_cast1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
                          ∀X,Y. T = ⓝY.X → ⦃G, L⦄ ⊢ X •[h, g] ⦃l, U⦄.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #X #Y #H destruct
-| #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #l #i #_ #_ #_ #X #Y #H destruct
-| #a #I #L #V #T #U #l #_ #X #Y #H destruct
-| #L #V #T #U #l #_ #X #Y #H destruct
-| #L #W #T #U #l #HTU #X #Y #H destruct //
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #X #Y #H destruct
+| #G #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct
+| #G #L #K #W #V #U #l #i #_ #_ #_ #X #Y #H destruct
+| #a #I #G #L #V #T #U #l #_ #X #Y #H destruct
+| #G #L #V #T #U #l #_ #X #Y #H destruct
+| #G #L #W #T #U #l #HTU #X #Y #H destruct //
 ]
-qed.
+qed-.
 
 (* Basic_1: was just: sty0_gen_cast *)
-lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃G, L⦄ ⊢ ⓝY.X •[h, g] ⦃l, U⦄ →
+lemma ssta_inv_cast1: ∀h,g,G,L,X,Y,U,l. ⦃G, L⦄ ⊢ ⓝY.X •[h, g] ⦃l, U⦄ →
                       ⦃G, L⦄ ⊢ X •[h, g] ⦃l, U⦄.
-/2 width=4/ qed-.
+/2 width=4 by ssta_inv_cast1_aux/ qed-.
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 0f035cf7c..27c12c465 100644
--- 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.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
index 00e512498..e51c4e805 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
@@ -12,22 +12,22 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/static/ssta.ma". (**) (* disambiguation error *)
 include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/static/ssta.ma".
 
 (* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
 
 (* Properties on relocation *************************************************)
 
 (* Basic_1: was just: sty0_lift *)
-lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
+lemma ssta_lift: ∀h,g,G,L1,T1,U1,l. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
                  ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 →
-                 ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄.
-#h #g #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l
-[ #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+                 ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄.
+#h #g #G #L1 #T1 #U1 #l #H elim H -G -L1 -T1 -U1 -l
+[ #G #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2
   >(lift_inv_sort1 … H1) -X1
   >(lift_inv_sort1 … H2) -X2 /2 width=1/
-| #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+| #G #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
   elim (lift_inv_lref1 … H) * #Hid #H destruct
   [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
     elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
@@ -36,7 +36,7 @@ lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
   | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
     lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
   ]
-| #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+| #G #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
   elim (lift_inv_lref1 … H) * #Hid #H destruct
   [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
     elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
@@ -46,27 +46,27 @@ lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
   | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
     lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
   ]
-| #a #I #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+| #a #I #G #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
   elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
   elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
   lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
-| #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+| #G #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
   elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
   elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
   lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
-| #L1 #W1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+| #G #L1 #W1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
   elim (lift_inv_flat1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct /3 width=5/
 ]
 qed.
 
 (* Note: apparently this was missing in basic_1 *)
-lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ →
+lemma ssta_inv_lift1: ∀h,g,G,L2,T2,U2,l. ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ →
                       ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 →
-                      ∃∃U1. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ & ⇧[d, e] U1 ≡ U2.
-#h #g #L2 #T2 #U2 #l #H elim H -L2 -T2 -U2 -l
-[ #L2 #k #l #Hkl #L1 #d #e #_ #X #H
+                      ∃∃U1. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ & ⇧[d, e] U1 ≡ U2.
+#h #g #G #L2 #T2 #U2 #l #H elim H -G -L2 -T2 -U2 -l
+[ #G #L2 #k #l #Hkl #L1 #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X /3 width=3/
-| #L2 #K2 #V2 #W2 #W #i #l #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H
+| #G #L2 #K2 #V2 #W2 #W #i #l #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H
   elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ]
   [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12
     elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12
@@ -78,7 +78,7 @@ lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2
     | <le_plus_minus_comm //
     ]
   ]
-| #L2 #K2 #W2 #V2 #W #i #l #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H
+| #G #L2 #K2 #W2 #V2 #W #i #l #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H
   elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HWV2 | -IHWV2 ]
   [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #W1 #HLK1 #HK21 #HW12
     elim (IHWV2 … HK21 … HW12) -K2 #V1 #HWV1 #_
@@ -90,33 +90,33 @@ lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2
     | <le_plus_minus_comm //
     ]
   ]
-| #a #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+| #a #I #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
   elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/
-| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+| #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
   elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/
-| #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+| #G #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
   elim (lift_inv_flat2 … H) -H #W1 #T1 #HW12 #HT12 #H destruct
   elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=3/
 ]
-qed.
+qed-.
 
 (* Advanced forvard lemmas **************************************************)
 
 (* Basic_1: was just: sty0_correct *)
-lemma ssta_fwd_correct: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
+lemma ssta_fwd_correct: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
                         ∃T0. ⦃G, L⦄ ⊢ U •[h, g] ⦃l-1, T0⦄.
-#h #g #L #T #U #l #H elim H -L -T -U -l
+#h #g #G #L #T #U #l #H elim H -G -L -T -U -l
 [ /4 width=2/
-| #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
+| #G #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
   elim (lift_total V0 0 (i+1)) /3 width=10/
-| #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
+| #G #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
   elim (lift_total V 0 (i+1)) /3 width=10/
-| #a #I #L #V #T #U #l #_ * /3 width=2/
-| #L #V #T #U #l #_ * #T0 #HUT0 /3 width=2/
-| #L #W #T #U #l #_ * /2 width=2/
+| #a #I #G #L #V #T #U #l #_ * /3 width=2/
+| #G #L #V #T #U #l #_ * #T0 #HUT0 /3 width=2/
+| #G #L #W #T #U #l #_ * /2 width=2/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
index 87e0d2168..8cc03442d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma
@@ -19,29 +19,29 @@ include "basic_2/static/ssta_lift.ma".
 (* Main properties **********************************************************)
 
 (* Note: apparently this was missing in basic_1 *)
-theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃G, L⦄ ⊢ T •[h, g] ⦃l1, U1⦄ →
+theorem ssta_mono: ∀h,g,G,L,T,U1,l1. ⦃G, L⦄ ⊢ T •[h, g] ⦃l1, U1⦄ →
                    ∀U2,l2. ⦃G, L⦄ ⊢ T •[h, g] ⦃l2, U2⦄ → l1 = l2 ∧ U1 = U2.
-#h #g #L #T #U1 #l1 #H elim H -L -T -U1 -l1
-[ #L #k #l #Hkl #X #l2 #H
+#h #g #G #L #T #U1 #l1 #H elim H -G -L -T -U1 -l1
+[ #G #L #k #l #Hkl #X #l2 #H
   elim (ssta_inv_sort1 … H) -H #Hkl2 #H destruct
   >(deg_mono … Hkl2 … Hkl) -g -L -l2 /2 width=1/
-| #L #K #V #W #U1 #i #l1 #HLK #_ #HWU1 #IHVW #U2 #l2 #H
+| #G #L #K #V #W #U1 #i #l1 #HLK #_ #HWU1 #IHVW #U2 #l2 #H
   elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0] #HLK0 #HVW0 #HW0U2
   lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
   lapply (IHVW … HVW0) -IHVW -HVW0 * #H1 #H2 destruct
   >(lift_mono … HWU1 … HW0U2) -W0 -U1 /2 width=1/
-| #L #K #W #V #U1 #i #l1 #HLK #_ #HWU1 #IHWV #U2 #l2 #H
+| #G #L #K #W #V #U1 #i #l1 #HLK #_ #HWU1 #IHWV #U2 #l2 #H
   elim (ssta_inv_lref1 … H) -H * #K0 #W0 #V0 [2: #l0 ] #HLK0 #HWV0 #HV0U2
   lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
   lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct
   >(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/
-| #a #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
+| #a #I #G #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
   elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct
   elim (IHTU1 … HTU2) -T /3 width=1/
-| #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
+| #G #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
   elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct
   elim (IHTU1 … HTU2) -T /3 width=1/
-| #L #W1 #T #U1 #l1 #_ #IHTU1 #U2 #l2 #H
+| #G #L #W1 #T #U1 #l1 #_ #IHTU1 #U2 #l2 #H
   lapply (ssta_inv_cast1 … H) -H #HTU2
   elim (IHTU1 … HTU2) -T /2 width=1/
 ]
@@ -49,8 +49,8 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma ssta_inv_refl_pos: ∀h,g,L,T,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, T⦄ → ⊥.
-#h #g #L #T #l #HTT
+lemma ssta_inv_refl_pos: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, T⦄ → ⊥.
+#h #g #G #L #T #l #HTT
 elim (ssta_fwd_correct … HTT) <minus_plus_m_m #U #HTU
 elim (ssta_mono … HTU … HTT) -h -L #H #_ -T -U
 elim (plus_xySz_x_false 0 l 0 ?) //
-- 
2.39.2