From d7ccf1bd91637d3c59a285df6f215ecfde2a2450 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 7 Aug 2013 21:38:40 +0000
Subject: [PATCH] passive support for global environments completed!

---
 .../lambdadelta/basic_2/dynamic/lsubsv.ma     |  92 +++++------
 .../basic_2/dynamic/lsubsv_cpcs.ma            |   6 +-
 .../basic_2/dynamic/lsubsv_cpds.ma            |  44 ++---
 .../basic_2/dynamic/lsubsv_ldrop.ma           |  12 +-
 .../basic_2/dynamic/lsubsv_lsuba.ma           |   4 +-
 .../lambdadelta/basic_2/dynamic/lsubsv_snv.ma |  24 +--
 .../basic_2/dynamic/lsubsv_ssta.ma            |  18 +-
 .../lambdadelta/basic_2/dynamic/snv.ma        | 151 ++++++++---------
 .../lambdadelta/basic_2/dynamic/snv_aaa.ma    |  16 +-
 .../lambdadelta/basic_2/dynamic/snv_cpcs.ma   | 156 +++++++++---------
 .../lambdadelta/basic_2/dynamic/snv_lift.ma   |  48 +++---
 .../lambdadelta/basic_2/dynamic/snv_lpr.ma    |  40 ++---
 .../lambdadelta/basic_2/dynamic/snv_ssta.ma   |  26 +--
 .../basic_2/dynamic/snv_ssta_lpr.ma           |  28 ++--
 .../lambdadelta/basic_2/dynamic/snv_sstas.ma  |   4 +-
 .../lambdadelta/basic_2/dynamic/ygt.ma        |  78 ++++-----
 .../lambdadelta/basic_2/dynamic/ygt_ygt.ma    |   4 +-
 .../lambdadelta/basic_2/dynamic/ypr.ma        |  18 +-
 .../lambdadelta/basic_2/dynamic/yprs.ma       |  70 ++++----
 .../lambdadelta/basic_2/dynamic/yprs_yprs.ma  |   4 +-
 .../lambdadelta/basic_2/dynamic/ysc.ma        |  27 +--
 .../relations/{btpred_6.ma => btpred_8.ma}    |   4 +-
 .../{btpredstar_6.ma => btpredproper_8.ma}    |   4 +-
 .../{btpredproper_6.ma => btpredstar_8.ma}    |   4 +-
 ...dstarproper_6.ma => btpredstarproper_8.ma} |   4 +-
 .../{nativevalid_4.ma => lrsubeqv_5.ma}       |   4 +-
 .../{lrsubeqv_4.ma => nativevalid_5.ma}       |   4 +-
 .../lambdadelta/basic_2/web/basic_2.ldw.xml   |   2 +-
 28 files changed, 449 insertions(+), 447 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{btpred_6.ma => btpred_8.ma} (83%)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{btpredstar_6.ma => btpredproper_8.ma} (82%)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{btpredproper_6.ma => btpredstar_8.ma} (82%)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{btpredstarproper_6.ma => btpredstarproper_8.ma} (82%)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{nativevalid_4.ma => lrsubeqv_5.ma} (88%)
 rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lrsubeqv_4.ma => nativevalid_5.ma} (87%)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
index 29d6151fe..0d39f32ec 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
@@ -12,104 +12,104 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/lrsubeqv_4.ma".
+include "basic_2/notation/relations/lrsubeqv_5.ma".
 include "basic_2/dynamic/snv.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
 
 (* Note: this is not transitive *)
-inductive lsubsv (h:sh) (g:sd h): relation lenv ≝
-| lsubsv_atom: lsubsv h g (⋆) (⋆)
-| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 →
-               lsubsv h g (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubsv_abbr: ∀L1,L2,W,V,W1,V2,l. ⦃h, L1⦄ ⊢ ⓝW.V ¡[h, g] → ⦃h, L2⦄ ⊢ W ¡[h, g] →
-               ⦃h, L1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ → ⦃h, L2⦄ ⊢ W •[h, g] ⦃l, V2⦄ →
-               lsubsv h g L1 L2 → lsubsv h g (L1.ⓓⓝW.V) (L2.ⓛW)
+inductive lsubsv (h) (g) (G): relation lenv ≝
+| lsubsv_atom: lsubsv h g G (⋆) (⋆)
+| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g G L1 L2 →
+               lsubsv h g G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubsv_abbr: ∀L1,L2,W,V,W1,V2,l. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, g] → ⦃G, L2⦄ ⊢ W ¡[h, g] →
+               ⦃G, L1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ → ⦃G, L2⦄ ⊢ W •[h, g] ⦃l, V2⦄ →
+               lsubsv h g G L1 L2 → lsubsv h g G (L1.ⓓⓝW.V) (L2.ⓛW)
 .
 
 interpretation
   "local environment refinement (stratified native validity)"
-  'LRSubEqV h g L1 L2 = (lsubsv h g L1 L2).
+  'LRSubEqV h g G L1 L2 = (lsubsv h g G L1 L2).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 = ⋆ → L2 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
+fact lsubsv_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → L1 = ⋆ → L2 = ⋆.
+#h #g #G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #V #_ #H destruct
 | #L1 #L2 #W #V #V1 #V2 #l #_ #_ #_ #_ #_ #H destruct
 ]
 qed-.
 
-lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ¡⊑[h, g] L2 → L2 = ⋆.
-/2 width=5 by lsubsv_inv_atom1_aux/ qed-.
+lemma lsubsv_inv_atom1: ∀h,g,G,L2. G ⊢ ⋆ ¡⊑[h, g] L2 → L2 = ⋆.
+/2 width=6 by lsubsv_inv_atom1_aux/ qed-.
 
-fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
+fact lsubsv_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
                            ∀I,K1,X. L1 = K1.ⓑ{I}X →
-                           (∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
-                           ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] &
-                                             ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
-                                             h ⊢ K1 ¡⊑[h, g] K2 &
+                           (∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
+                           ∃∃K2,W,V,W1,V2,l. ⦃G, K1⦄ ⊢ X ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+                                             ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
+                                             G ⊢ K1 ¡⊑[h, g] K2 &
                                              I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-#h #g #L1 #L2 * -L1 -L2
+#h #g #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 #W1 #V2 #l #HV #HW #HW1 #HV2 #HL12 #J #K1 #X #H destruct /3 width=12/
 ]
 qed-.
 
-lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,X. h ⊢ K1.ⓑ{I}X ¡⊑[h, g] L2 →
-                        (∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
-                        ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] &
-                                          ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
-                                          h ⊢ K1 ¡⊑[h, g] K2 &
+lemma lsubsv_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ¡⊑[h, g] L2 →
+                        (∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
+                        ∃∃K2,W,V,W1,V2,l. ⦃G, K1⦄ ⊢ X ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+                                          ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
+                                          G ⊢ K1 ¡⊑[h, g] K2 &
                                           I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
 /2 width=3 by lsubsv_inv_pair1_aux/ qed-.
 
-fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L2 = ⋆ → L1 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
+fact lsubsv_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → L2 = ⋆ → L1 = ⋆.
+#h #g #G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #V #_ #H destruct
 | #L1 #L2 #W #V #V1 #V2 #l #_ #_ #_ #_ #_ #H destruct
 ]
 qed-.
 
-lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ¡⊑[h, g] ⋆ → L1 = ⋆.
-/2 width=5 by lsubsv_inv_atom2_aux/ qed-.
+lemma lsubsv_inv_atom2: ∀h,g,G,L1. G ⊢ L1 ¡⊑[h, g] ⋆ → L1 = ⋆.
+/2 width=6 by lsubsv_inv_atom2_aux/ qed-.
 
-fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
+fact lsubsv_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
                            ∀I,K2,W. L2 = K2.ⓑ{I}W →
-                           (∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
-                           ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] &
-                                           ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
-                                           h ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
-#h #g #L1 #L2 * -L1 -L2
+                           (∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
+                           ∃∃K1,V,W1,V2,l. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+                                           ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
+                                           G ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+#h #g #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 #W1 #V2 #l #HV #HW #HW1 #HV2 #HL12 #J #K2 #U #H destruct /3 width=10/
 ]
 qed-.
 
-lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 ¡⊑[h, g] K2.ⓑ{I}W →
-                        (∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
-                        ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] &
-                                        ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
-                                        h ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ¡⊑[h, g] K2.ⓑ{I}W →
+                        (∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
+                        ∃∃K1,V,W1,V2,l. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] &
+                                        ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ &
+                                        G ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
 /2 width=3 by lsubsv_inv_pair2_aux/ qed-.
 
 (* Basic_forward lemmas *****************************************************)
 
-lemma lsubsv_fwd_lsubr: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 ⊑ L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+lemma lsubsv_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → L1 ⊑ L2.
+#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lsubsv_refl: ∀h,g,L. h ⊢ L ¡⊑[h, g] L.
-#h #g #L elim L -L // /2 width=1/
+lemma lsubsv_refl: ∀h,g,G,L. G ⊢ L ¡⊑[h, g] L.
+#h #g #G #L elim L -L // /2 width=1/
 qed.
 
-lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
-                         ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-/3 width=5 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
+lemma lsubsv_cprs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
+                         ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2.
+/3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
index 30e42ea09..03ef9527c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
@@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv.ma".
 
 (* Properties on context-sensitive parallel equivalence for terms ***********)
 
-lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
-                         ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
-/3 width=5 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/
+lemma lsubsv_cpcs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
+                         ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
+/3 width=6 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma
index 55a7e9a13..d9b21a9f6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma
@@ -19,38 +19,38 @@ include "basic_2/dynamic/lsubsv_ssta.ma".
 
 (* Properties for the preservation results **********************************)
 
-fact lsubsv_sstas_aux: ∀h,g,L0,T0.
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
-                       ∀L2,T. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊢ T ¡[h, g] →
-                       ∀L1. h ⊢ L1 ¡⊑[h, g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[h, g] U2 →
-                       ∃∃U1. ⦃h, L1⦄ ⊢ T •*[h, g] U1 & L1 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T #HLT0 #HT #L1 #HL12 #U2 #H @(sstas_ind … H) -U2 [ /2 width=3/ ]
+fact lsubsv_sstas_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) →
+                       ∀G,L2,T. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L2, T⦄ → ⦃G, L2⦄ ⊢ T ¡[h, g] →
+                       ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → ∀U2. ⦃G, L2⦄ ⊢ T •*[h, g] U2 →
+                       ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, g] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L2 #T #HLT0 #HT #L1 #HL12 #U2 #H @(sstas_ind … H) -U2 [ /2 width=3/ ]
 #U2 #W #l #HTU2 #HU2W * #U1 #HTU1 #HU12
 lapply (IH1 … HT … HL12) // #H
-lapply (snv_sstas_aux … IH2 … HTU1) // /3 width=4 by ygt_yprs_trans, lsubsv_yprs/ -H #HU1
+lapply (snv_sstas_aux … IH2 … HTU1) // /3 width=5 by ygt_yprs_trans, lsubsv_yprs/ -H #HU1
 lapply (snv_sstas_aux … IH2 … HTU2) // #H
-lapply (IH1 … H … HL12) [ /3 width=4 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2
+lapply (IH1 … H … HL12) [ /3 width=5 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2
 elim (snv_fwd_ssta … HU1) #l1 #W1 #HUW1
 elim (lsubsv_ssta_trans … HU2W … HL12) -HU2W #W2 #HUW2 #HW2
 elim (ssta_cpcs_lpr_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12 L1) -HU1 -HU2 -HUW2 -HU12 //
-[2,3: /4 width=4 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -L2 -L0 -T0 -U2 #H #HW12 destruct
+[2,3: /4 width=5 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -G0 -L2 -L0 -T0 -U2 #H #HW12 destruct
 lapply (cpcs_trans … HW12 … HW2) -W2 /3 width=4/
 qed-.
 
-fact lsubsv_cpds_aux: ∀h,g,L0,T0.
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
-                      ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊢ T1 ¡[h, g] →
-                      ∀L1. h ⊢ L1 ¡⊑[h, g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[h, g] T2 →
-                      ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[h, g] T & L1 ⊢ T2 ➡* T.
-#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2
+fact lsubsv_cpds_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) →
+                      ∀G,L2,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G,L2, T1⦄ → ⦃G, L2⦄ ⊢ T1 ¡[h, g] →
+                      ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → ∀T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 →
+                      ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2
 lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2
-elim (lsubsv_sstas_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0
+elim (lsubsv_sstas_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -G0 -L2 -L0 -T0 #T0 #HT10 #HT0
 lapply (cpcs_cprs_strap1 … HT0 … HTT2) -T #HT02
 elim (cpcs_inv_cprs … HT02) -HT02 /3 width=3/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
index 31d47c8c5..6d0e6d42d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma
@@ -19,10 +19,10 @@ include "basic_2/dynamic/lsubsv.ma".
 (* Properties concerning basic local environment slicing ********************)
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
+lemma lsubsv_ldrop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
                             ∀K1,e. ⇩[0, e] L1 ≡ K1 →
-                            ∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L2 ≡ K2.
-#h #g #L1 #L2 #H elim H -L1 -L2
+                            ∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L2 ≡ K2.
+#h #g #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
@@ -42,10 +42,10 @@ lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
 qed-.
 
 (* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 →
+lemma lsubsv_ldrop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
                              ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                             ∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L1 ≡ K1.
-#h #g #L1 #L2 #H elim H -L1 -L2
+                             ∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L1 ≡ K1.
+#h #g #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/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
index 7d40d4081..27da78fca 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
@@ -19,8 +19,8 @@ include "basic_2/dynamic/lsubsv.ma".
 
 (* Forward lemmas on lenv refinement for atomic arity assignment ************)
 
-lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 ⁝⊑ L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → G ⊢ L1 ⁝⊑ L2.
+#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
 #L1 #L2 #W #V #W1 #V2 #l #HV #HW #_ #_ #_ #IHL12 -W1 -V2
 elim (snv_fwd_aaa … HV) -HV #A #HV
 elim (snv_fwd_aaa … HW) -HW #B #HW
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
index 67230d980..840e4a31a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
@@ -20,14 +20,14 @@ include "basic_2/dynamic/lsubsv_cpcs.ma".
 
 (* Properties concerning stratified native validity *************************)
 
-fact snv_lsubsv_aux: ∀h,g,L0,T0.
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                     (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
-                     ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_lsubsv h g L1 T1.
-#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 * * [||||*] //
-[ #i #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
+fact snv_lsubsv_aux: ∀h,g,G0,L0,T0.
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) →
+                     ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lsubsv h g G1 L1 T1.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L2 * * [||||*] //
+[ #i #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
   elim (snv_inv_lref … H) -H #I2 #K2 #W2 #HLK2 #HW2
   elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -HL12 #X #H #HLK1
   elim (lsubsv_inv_pair2 … H) -H * #K1
@@ -35,11 +35,11 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0.
     /5 width=8 by snv_lref, fsupp_ygt, fsupp_lref/ (**) (* auto too slow without trace *)
   | #V #W1 #V2 #l #HV #_ #_ #_ #_ #_ #H destruct /2 width=5/
   ]
-| #p #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1
+| #p #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H)
-| #a #I #V #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
+| #a #I #V #T #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
   elim (snv_inv_bind … H) -H /4 width=4/
-| #V #T #HL0 #HT0 #H #L1 #HL12 destruct
+| #V #T #HG0 #HL0 #HT0 #H #L1 #HL12 destruct
   elim (snv_inv_appl … H) -H #a #W #W0 #U #l #HV #HT #HVW #HW0 #HTU
   lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0
   elim (lsubsv_ssta_trans … HVW … HL12) -HVW #W1 #HVW1 #HW1
@@ -50,7 +50,7 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0.
   elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0
   lapply (cpds_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0
   /4 width=8 by snv_appl, fsupp_ygt/ (**) (* auto too slow without trace *)
-| #W #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
+| #W #T #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
   elim (snv_inv_cast … H) -H #U #l #HW #HT #HTU #HUW
   lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW
   elim (lsubsv_ssta_trans … HTU … HL12) -HTU #U0 #HTU0 #HU0
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
index 15f2e14b7..dc922ff54 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma
@@ -20,12 +20,12 @@ include "basic_2/dynamic/lsubsv_ldrop.ma".
 
 (* Properties on stratified static type assignment **************************)
 
-lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[h, g] ⦃l, U2⦄ →
-                         ∀L1. h ⊢ L1 ¡⊑[h, g] L2 →
-                         ∃∃U1. ⦃h, L1⦄ ⊢ T •[h, g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.
-#h #g #L2 #T #U #l #H elim H -L2 -T -U -l
+lemma lsubsv_ssta_trans: ∀h,g,G,L2,T,U2,l. ⦃G, L2⦄ ⊢ T •[h, g] ⦃l, U2⦄ →
+                         ∀L1. G ⊢ L1 ¡⊑[h, g] L2 →
+                         ∃∃U1. ⦃G, L1⦄ ⊢ T •[h, g] ⦃l, U1⦄ & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L2 #T #U #l #H elim H -G -L2 -T -U -l
 [ /3 width=3/
-| #L2 #K2 #X #Y #U #i #l #HLK2 #_ #HYU #IHXY #L1 #HL12
+| #G #L2 #K2 #X #Y #U #i #l #HLK2 #_ #HYU #IHXY #L1 #HL12
   elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
   elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HYU -IHXY -HLK1 ]
   [ #HK12 #H destruct
@@ -34,7 +34,7 @@ lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[h, g] ⦃l, U2
     elim (lift_total T 0 (i+1)) /3 width=11/
   | #V #W1 #V2 #l0 #_ #_ #_ #_ #_ #H destruct
   ]
-| #L2 #K2 #Y #X #U #i #l #HLK2 #HYX #HYU #IHYX #L1 #HL12
+| #G #L2 #K2 #Y #X #U #i #l #HLK2 #HYX #HYU #IHYX #L1 #HL12
   elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
   elim (lsubsv_inv_pair2 … H) -H * #K1 [ -HYX | -IHYX ]
   [ #HK12 #H destruct
@@ -47,11 +47,11 @@ lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[h, g] ⦃l, U2
     elim (lift_total W 0 (i+1))
     /4 width=11 by cpcs_lift, ex2_intro, ssta_ldef, ssta_cast/
   ]
-| #a #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
+| #a #I #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
   elim (IHTU2 (L1.ⓑ{I}V2) …) [2: /2 width=1/ ] -L2 /3 width=3/
-| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
+| #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
   elim (IHTU2 … HL12) -L2 /3 width=5/
-| #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
+| #G #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
   elim (IHTU2 … HL12) -L2 /3 width=3/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
index 3f62cff77..a60c3cd7d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma
@@ -12,118 +12,119 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/nativevalid_4.ma".
+include "basic_2/notation/relations/nativevalid_5.ma".
 include "basic_2/computation/cpds.ma".
 include "basic_2/equivalence/cpcs.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
 
-inductive snv (h:sh) (g:sd h): lenv → predicate term ≝
-| snv_sort: ∀L,k. snv h g L (⋆k)
-| snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i)
-| snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T)
-| snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
+(* activate genv *)
+inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝
+| snv_sort: ∀G,L,k. snv h g G L (⋆k)
+| snv_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i)
+| snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T)
+| snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T →
             ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ → ⦃G, L⦄ ⊢ W ➡* W0 →
-            ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
-| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
-            ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ U ⬌* W → snv h g L (ⓝW.T)
+            ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g G L (ⓐV.T)
+| snv_cast: ∀G,L,W,T,U,l. snv h g G L W → snv h g G L T →
+            ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T)
 .
 
 interpretation "stratified native validity (term)"
-   'NativeValid h g L T = (snv h g L T).
+   'NativeValid h g G L T = (snv h g G L T).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact snv_inv_lref_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i →
-                       ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ¡[h, g].
-#h #g #L #X * -L -X
-[ #L #k #i #H destruct
-| #I #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/
-| #a #I #L #V #T #_ #_ #i #H destruct
-| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #i #H destruct
-| #L #W #T #U #l #_ #_ #_ #_ #i #H destruct
+fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i →
+                       ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
+#h #g #G #L #X * -G -L -X
+[ #G #L #k #i #H destruct
+| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/
+| #a #I #G #L #V #T #_ #_ #i #H destruct
+| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #i #H destruct
+| #G #L #W #T #U #l #_ #_ #_ #_ #i #H destruct
 ]
-qed.
-
-lemma snv_inv_lref: ∀h,g,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] →
-                    ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ¡[h, g].
-/2 width=3/ qed-.
-
-fact snv_inv_gref_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥.
-#h #g #L #X * -L -X
-[ #L #k #p #H destruct
-| #I #L #K #V #i #_ #_ #p #H destruct
-| #a #I #L #V #T #_ #_ #p #H destruct
-| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #p #H destruct
-| #L #W #T #U #l #_ #_ #_ #_ #p #H destruct
+qed-.
+
+lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] →
+                    ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
+/2 width=3 by snv_inv_lref_aux/ qed-.
+
+fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥.
+#h #g #G #L #X * -G -L -X
+[ #G #L #k #p #H destruct
+| #I #G #L #K #V #i #_ #_ #p #H destruct
+| #a #I #G #L #V #T #_ #_ #p #H destruct
+| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #p #H destruct
+| #G #L #W #T #U #l #_ #_ #_ #_ #p #H destruct
 ]
-qed.
-
-lemma snv_inv_gref: ∀h,g,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥.
-/2 width=7/ qed-.
-
-fact snv_inv_bind_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
-                       ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
-#h #g #L #X * -L -X
-[ #L #k #a #I #V #T #H destruct
-| #I0 #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
-| #b #I0 #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/
-| #b #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct
-| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #a #I #V #T #H destruct
+qed-.
+
+lemma snv_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥.
+/2 width=8 by snv_inv_gref_aux/ qed-.
+
+fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
+                       ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
+#h #g #G #L #X * -G -L -X
+[ #G #L #k #a #I #V #T #H destruct
+| #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
+| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/
+| #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct
+| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #a #I #V #T #H destruct
 ]
-qed.
+qed-.
 
-lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] →
-                        ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
-/2 width=4/ qed-.
+lemma snv_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] →
+                        ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g].
+/2 width=4 by snv_inv_bind_aux/ qed-.
 
-fact snv_inv_appl_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T →
+fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T →
                        ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
                                    ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ & ⦃G, L⦄ ⊢ W ➡* W0 &
                                    ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
-#h #g #L #X * -L -X
-[ #L #k #V #T #H destruct
-| #I #L #K #V0 #i #_ #_ #V #T #H destruct
-| #a #I #L #V0 #T0 #_ #_ #V #T #H destruct
-| #a #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8/
-| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #V #T #H destruct
+#h #g #G #L #X * -L -X
+[ #G #L #k #V #T #H destruct
+| #I #G #L #K #V0 #i #_ #_ #V #T #H destruct
+| #a #I #G #L #V0 #T0 #_ #_ #V #T #H destruct
+| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8/
+| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #V #T #H destruct
 ]
-qed.
+qed-.
 
-lemma snv_inv_appl: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] →
+lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] →
                     ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
                                 ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ & ⦃G, L⦄ ⊢ W ➡* W0 &
                                 ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U.
-/2 width=3/ qed-.
+/2 width=3 by snv_inv_appl_aux/ qed-.
 
-fact snv_inv_cast_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T →
+fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T →
                        ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
                               ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ & ⦃G, L⦄ ⊢ U ⬌* W.
-#h #g #L #X * -L -X
-[ #L #k #W #T #H destruct
-| #I #L #K #V #i #_ #_ #W #T #H destruct
-| #a #I #L #V #T0 #_ #_ #W #T #H destruct
-| #a #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct
-| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HUW0 #W #T #H destruct /2 width=4/
+#h #g #G #L #X * -G -L -X
+[ #G #L #k #W #T #H destruct
+| #I #G #L #K #V #i #_ #_ #W #T #H destruct
+| #a #I #G #L #V #T0 #_ #_ #W #T #H destruct
+| #a #G #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct
+| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HUW0 #W #T #H destruct /2 width=4/
 ]
-qed.
+qed-.
 
-lemma snv_inv_cast: ∀h,g,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] →
+lemma snv_inv_cast: ∀h,g,G,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] →
                     ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] &
                            ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ & ⦃G, L⦄ ⊢ U ⬌* W.
-/2 width=3/ qed-.
+/2 width=3 by snv_inv_cast_aux/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma snv_fwd_ssta: ∀h,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃∃l,U. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄.
-#h #g #L #T #H elim H -L -T
-[ #L #k elim (deg_total h g k) /3 width=3/
-| * #L #K #V #i #HLK #_ * #l0 #W #HVW
+lemma snv_fwd_ssta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃∃l,U. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄.
+#h #g #G #L #T #H elim H -G -L -T
+[ #G #L #k elim (deg_total h g k) /3 width=3/
+| * #G #L #K #V #i #HLK #_ * #l0 #W #HVW
   [ elim (lift_total W 0 (i+1)) /3 width=8/
   | elim (lift_total V 0 (i+1)) /3 width=8/
   ]
-| #a #I #L #V #T #_ #_ #_ * /3 width=3/
-| #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/
-| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *)
+| #a #I #G #L #V #T #_ #_ #_ * /3 width=3/
+| #a #G #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/
+| #G #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *)
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
index 3a161e1f9..6a823189a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma
@@ -21,21 +21,21 @@ include "basic_2/dynamic/snv.ma".
 
 (* Forward lemmas on atomic arity assignment for terms **********************)
 
-lemma snv_fwd_aaa: ∀h,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A.
-#h #g #L #T #H elim H -L -T
+lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A.
+#h #g #G #L #T #H elim H -G -L -T
 [ /2 width=2/
-| #I #L #K #V #i #HLK #_ * /3 width=6/
-| #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/
-| #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT
+| #I #G #L #K #V #i #HLK #_ * /3 width=6/
+| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/
+| #a #G #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT
   lapply (cpds_aaa h g … HV W0 ?) [ -HTU /3 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *)
   lapply (cpds_aaa … HT … HTU) -HTU #H
   elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
   lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/
-| #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT
+| #G #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT
   lapply (aaa_cpcs_mono … HUW A … HW) -HUW /2 width=7/ -HTU #H destruct /3 width=3/
 ]
 qed-.
 
-lemma snv_fwd_csn: ∀h,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/
+lemma snv_fwd_csn: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
index 8aaf788a2..d5d16cafa 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma
@@ -21,64 +21,64 @@ include "basic_2/dynamic/ygt.ma".
 
 (* Inductive premises for the preservation results **************************)
 
-definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation2 lenv term ≝
-                           λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[h, g] →
-                           ∀T2. L1 ⊢ T1 ➡ T2 → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ T2 ¡[h, g].
-
-definition IH_ssta_cpr_lpr: ∀h:sh. sd h → relation2 lenv term ≝
-                            λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[h, g] →
-                            ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
-                            ∀T2. L1 ⊢ T1 ➡ T2 → ∀L2. L1 ⊢ ➡ L2 →
-                            ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
-
-definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝
-                        λh,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
+definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+                           λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                           ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+
+definition IH_ssta_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+                            λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                            ∀U1,l. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
+                            ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                            ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+
+definition IH_snv_ssta: ∀h:sh. sd h → relation3 genv lenv term ≝
+                        λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
                         ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ U ¡[h, g].
 
-definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝
-                          λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[h, g] →
-                          ∀L1. h ⊢ L1 ¡⊑[h, g] L2 → ⦃h, L1⦄ ⊢ T ¡[h, g].
+definition IH_snv_lsubsv: ∀h:sh. sd h → relation3 genv lenv term ≝
+                          λh,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] →
+                          ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g].
 
 (* Properties for the preservation results **********************************)
 
-fact snv_cprs_lpr_aux: ∀h,g,L0,T0.
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                       ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] →
-                       ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ T2 ¡[h, g].
-#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #T2 #H
+fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
 elim H -T2 [ /2 width=6/ ] -HT1
 /4 width=6 by ygt_yprs_trans, cprs_yprs/
 qed-.
 
-fact ssta_cprs_lpr_aux: ∀h,g,L0,T0.
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                        ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] →
-                        ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
-                        ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 →
-                        ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H
+fact ssta_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                        ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                        ∀U1,l. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
+                        ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                        ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H
 elim H -T2 [ /2 width=7/ ]
 #T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
 elim (IHT1 L1) // -IHT1 #U #HTU #HU1
 elim (IH1 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
-[2: /3 width=9 by snv_cprs_lpr_aux/
+[2: /3 width=10 by snv_cprs_lpr_aux/
 |3: /5 width=6 by ygt_yprs_trans, cprs_yprs/
-] -L0 -T0 -T1 -T #U2 #HTU2 #HU2
+] -G0 -L0 -T0 -T1 -T #U2 #HTU2 #HU2
 lapply (lpr_cpcs_conf … HL12 … HU1) -L1 #HU1
 lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/
 qed-.
 
-fact ssta_cpcs_lpr_aux: ∀h,g,L0,T0.
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                        ∀L1,T1,T2. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T2⦄ →
-                        ⦃h, L1⦄ ⊢ T1 ¡[h, g] → ⦃h, L1⦄ ⊢ T2 ¡[h, g] →
-                        ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ →
-                        ∀U2,l2. ⦃h, L1⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄ →
-                        L1 ⊢ T1 ⬌* T2 → ∀L2. L1 ⊢ ➡ L2 →
-                        l1 = l2 ∧ L2 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12
+fact ssta_cpcs_lpr_aux: ∀h,g,G0,L0,T0.
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                        ∀G,L1,T1,T2. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T2⦄ →
+                        ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+                        ∀U1,l1. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ →
+                        ∀U2,l2. ⦃G, L1⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄ →
+                        ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                        l1 = l2 ∧ ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12
 elim (cpcs_inv_cprs … H) -H #T #H1 #H2
 elim (ssta_cprs_lpr_aux … H01 HT1 … HTU1 … H1 … HL12) -T1 /2 width=1/ #W1 #H1 #HUW1
 elim (ssta_cprs_lpr_aux … H02 HT2 … HTU2 … H2 … HL12) -T2 /2 width=1/ #W2 #H2 #HUW2 -L0 -T0
@@ -86,71 +86,71 @@ elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct
 lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/
 qed-.
 
-fact snv_sstas_aux: ∀h,g,L0,T0.
-                    (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                    ∀L,T. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
+fact snv_sstas_aux: ∀h,g,G0,L0,T0.
+                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                    ∀G,L,T. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
                     ∀U. ⦃G, L⦄ ⊢ T •*[h, g] U → ⦃G, L⦄ ⊢ U ¡[h, g].
-#h #g #L0 #T0 #IH #L #T #H01 #HT #U #H
+#h #g #G0 #L0 #T0 #IH #G #L #T #H01 #HT #U #H
 @(sstas_ind … H) -U // -HT /4 width=5 by ygt_yprs_trans, sstas_yprs/
 qed-.
 
-fact snv_sstas_lpr_aux: ∀h,g,L0,T0.
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                        ∀L1,T. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T⦄ → ⦃h, L1⦄ ⊢ T ¡[h, g] →
-                        ∀U. ⦃h, L1⦄ ⊢ T •*[h, g] U → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ U ¡[h, g].
-/4 width=7 by snv_sstas_aux, ygt_yprs_trans, sstas_yprs/
+fact snv_sstas_lpr_aux: ∀h,g,G0,L0,T0.
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                        ∀G,L1,T. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T⦄ → ⦃G, L1⦄ ⊢ T ¡[h, g] →
+                        ∀U. ⦃G, L1⦄ ⊢ T •*[h, g] U → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U ¡[h, g].
+/4 width=8 by snv_sstas_aux, ygt_yprs_trans, sstas_yprs/
 qed-.
 
-fact sstas_cprs_lpr_aux: ∀h,g,L0,T0.
-                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                         (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                         ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] →
-                         ∀U1. ⦃h, L1⦄ ⊢ T1 •*[h, g] U1 → ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 →
-                         ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[h, g] U2 & L2 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #H
+fact sstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                         ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                         ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                         ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #H
 @(sstas_ind … H) -U1 [ /3 width=5 by lpr_cprs_conf, ex2_intro/ ]
 #U1 #W1 #l1 #HTU1 #HUW1 #IHTU1 #T2 #HT12 #L2 #HL12
 elim (IHTU1 … HT12 … HL12) -IHTU1 #U2 #HTU2 #HU12
 lapply (snv_cprs_lpr_aux … IH2 … HT1 … HT12 … HL12) // #HT2
 elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2
 elim (IH1 … HUW1 U1 … HL12) -HUW1 //
-[2: /3 width=7 by snv_sstas_aux/
-|3: /3 width=4 by ygt_yprs_trans, sstas_yprs/
+[2: /3 width=8 by snv_sstas_aux/
+|3: /3 width=5 by ygt_yprs_trans, sstas_yprs/
 ] #W #HU1W #HW1
 elim (ssta_cpcs_lpr_aux … IH2 IH1 … HU1W … HUW2 … HU12 L2) // -IH1 -HU1W -HU12
-[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, cprs_lpr_yprs/
-|3: /3 width=10 by snv_sstas_lpr_aux/
+[2: /4 width=9 by snv_sstas_aux, ygt_yprs_trans, cprs_lpr_yprs/
+|3: /3 width=11 by snv_sstas_lpr_aux/
 |4,5: /4 width=5 by ygt_yprs_trans, cprs_lpr_yprs, sstas_yprs/
-] -L0 -T0 -L1 -T1 -HT2 #H #HW12 destruct
+] -G0 -L0 -T0 -L1 -T1 -HT2 #H #HW12 destruct
 lapply (cpcs_trans … HW1 … HW12) -W /3 width=4/
 qed-.
 
-fact cpds_cprs_lpr_aux: ∀h,g,L0,T0.
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                        (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                        ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] →
-                        ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
-                        ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 →
-                        ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[h, g] U2 & L2 ⊢ U1 ➡* U2.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+fact cpds_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                        ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                        ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
+                        ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                        ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
 elim (sstas_cprs_lpr_aux … IH3 IH2 IH1 … H01 … HTW1 … HT12 … HL12) // -L0 -T0 -T1 #W2 #HTW2 #HW12
 lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
 elim (cpcs_inv_cprs … H) -H /3 width=3/
 qed-.
 
-fact ssta_cpds_aux: ∀h,g,L0,T0.
-                    (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                    (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                    ∀L,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+fact ssta_cpds_aux: ∀h,g,G0,L0,T0.
+                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                    ∀G,L,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
                     ∀l,U1. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l+1, U1⦄ → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 →
                     ∃∃U,U2. ⦃G, L⦄ ⊢ U1 •*[h, g] U & ⦃G, L⦄ ⊢ T2 •*[h, g] U2 & ⦃G, L⦄ ⊢ U ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
 elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ]
-[ elim (ssta_cprs_lpr_aux … IH2 IH1 … HTU1 … HTT2 L) // -L0 -T0 -T /3 width=5/
+[ elim (ssta_cprs_lpr_aux … IH2 IH1 … HTU1 … HTT2 L) // -G0 -L0 -T0 -T /3 width=5/
 | @(ex3_2_intro …T2 HU1T) // /2 width=1/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index 9b9513f0a..34e6c2db9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -20,77 +20,77 @@ include "basic_2/dynamic/snv.ma".
 
 (* Relocation properties ****************************************************)
 
-lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ T ¡[h, g] → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,d,e. ⇩[d, e] L ≡ K →
                 ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g].
-#h #g #K #T #H elim H -K -T
-[ #K #k #L #d #e #_ #X #H
+#h #g #G #K #T #H elim H -G -K -T
+[ #G #K #k #L #d #e #_ #X #H
   >(lift_inv_sort1 … H) -X -K -d -e //
-| #I #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H
+| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H
   elim (lift_inv_lref1 … H) * #Hid #H destruct
   [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2/ #X #HL0 #H
     elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #L0 #W #HLK0 #HVW #H destruct
     /3 width=8/
   | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // -Hid /3 width=8/
   ]
-| #a #I #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H
+| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H
   elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct
   /4 width=4/
-| #a #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H
+| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H
   elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
   elim (lift_total V0 d e) #W0 #HVW0
   elim (lift_total V1 d e) #W1 #HVW1
   elim (lift_total T1 (d+1) e) #U1 #HTU1
   @(snv_appl … a … W0 … W1 … U1 l)
   [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ]
-  @(cpds_lift … HLK … HTU … HT1) /2 width=1/
-| #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H
+  @(cpds_lift … HT1 … HLK … HTU) /2 width=1/
+| #G #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H
   elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct
   elim (lift_total V d e) #W #HVW
   @(snv_cast … W l) [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ]
 ]
 qed.
 
-lemma snv_inv_lift: ∀h,g,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,d,e. ⇩[d, e] L ≡ K →
-                    ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ T ¡[h, g].
-#h #g #L #U #H elim H -L -U
-[ #L #k #K #d #e #_ #X #H
+lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,d,e. ⇩[d, e] L ≡ K →
+                    ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g].
+#h #g #G #L #U #H elim H -G -L -U
+[ #G #L #k #K #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X -L -d -e //
-| #I #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H
+| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H
   elim (lift_inv_lref2 … H) * #Hid #H destruct
   [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2/ #X #HK0 #H
     elim (ldrop_inv_skip1 … H) -H /2 width=1/ -Hid #K0 #V #HLK0 #HVW #H destruct
     /3 width=8/
   | lapply (ldrop_conf_ge … HLK … HL0 ?) -L // -Hid /3 width=8/
   ]
-| #a #I #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H
+| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H
   elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
-| #a #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H
+| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
   elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0
   elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01
-  elim (cpds_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU
+  elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU
   elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct
   lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/
-| #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
+| #G #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
   elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct
   elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW
-  lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/
+  lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W /3 width=4/
 ]
 qed-.
 
 (* Advanced properties ******************************************************)
 
-lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
-                     ⦃h, L1⦄ ⊢ T1 ¡[h, g] → ⦃h, L2⦄ ⊢ T2 ¡[h, g].
-#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
-[ #I1 #L1 #V1 #H
+lemma snv_fsup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                     ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I1 #G1 #L1 #V1 #H
   elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
   lapply (ldrop_inv_O2 … H) -H #H destruct //
 |2: *
 |5,6: /3 width=7 by snv_inv_lift/
 ]
-[1,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
-|2,4: * #L1 #V1 #T1 #H
+[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
+|2,4: * #G1 #L1 #V1 #T1 #H
   [1,3: elim (snv_inv_appl … H) -H //
   |2,4: elim (snv_inv_cast … H) -H //
   ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
index 3007d7d67..8623b0f46 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -20,20 +20,20 @@ include "basic_2/dynamic/snv_cpcs.ma".
 
 (* Properties on context-free parallel reduction for local environments *****)
 
-fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                      (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                      ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g L1 T1.
-#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*]
-[ #k #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
+fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                      ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g G1 L1 T1.
+#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [||||*]
+[ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
   >(cpr_inv_sort1 … H2) -X //
-| #i #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+| #i #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
   elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
   elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
   elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-  lapply (fsupp_lref … HLK1) #HKL
+  lapply (fsupp_lref … G1 … HLK1) #HKL
   elim (cpr_inv_lref1 … H2) -H2
   [ #H destruct -HLK1
     lapply (IH1 … HV12 … HK12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HKL /2 width=5/
@@ -42,9 +42,9 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
     lapply (IH1 … HVW0 … HK12) -IH1 -HVW0 -HK12 // -HV1 [ /2 width=1/ ] -HKL /3 width=7/
   ]
-| #p #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
+| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2
   elim (snv_inv_bind … H1) -H1 #HV1 #HT1
   elim (cpr_inv_bind1 … H2) -H2 *
   [ #V2 #T2 #HV12 #HT12 #H destruct
@@ -54,7 +54,7 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (IH1 … HT1 … HT12 (L2.ⓓV1) ?) -IH1 [1,2: /2 width=1/ ] -L1 -T1 #HT2
     lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/
   ]
-| #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
   elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
   elim (cpr_inv_appl1 … H2) -H2 *
   [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
@@ -80,7 +80,7 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (IH1 … HW202 … HL12) // [ /2 width=1/ ] -HW20 #HW2
     lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) [1,2: /2 width=1/ ] -HT20 #HT2
     lapply (IH2 … HV2W3) //
-    [ @(ygt_yprs_trans … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *)
+    [ @(ygt_yprs_trans … G1 G1 … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *)
       [ /2 width=1 by fsupp_ygt/
       | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
       ]
@@ -89,8 +89,8 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
     elim (ssta_fwd_correct … HV2W3) <minus_plus_m_m #U3 #HWU3
     elim (ssta_cpcs_lpr_aux … IH1 IH3 … HWU3 … HWU2 … HW32 … L2) // -IH3
     [2: /4 width=5 by ygt_yprs_trans, fsupp_ygt, cprs_lpr_yprs, cpr_cprs/
-    |3: @(ygt_yprs_trans … L1 L2 … V2) (**) (* auto not tried *)
-        [ @(ygt_yprs_trans … L1 L1 … V1)
+    |3: @(ygt_yprs_trans … G1 G1 L1 L2 … V2) (**) (* auto not tried *)
+        [ @(ygt_yprs_trans … G1 G1 L1 L1 … V1)
           [ /2 width=1 by fsupp_ygt/
           | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
           ]
@@ -99,8 +99,8 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
     ] #H #_  destruct -IH2 -U3
     lapply (IH4 … HT2 (L2.ⓓⓝW2.V2) ?)
     [ /3 width=5/
-    | @(ygt_yprs_trans … (L1.ⓛW20) … T2) (**) (* auto /5 width=5/ is too slow even with trace timeout=35 *)
-      [ /4 width=4 by ygt_yprs_trans, fsupp_ygt, ypr_yprs, ypr_cpr/
+    | @(ygt_yprs_trans … G1 G1 … (L1.ⓛW20) … T2) (**) (* auto /5 width=5/ is too slow even with trace timeout=35 *)
+      [ /4 width=5 by ygt_yprs_trans, fsupp_ygt, ypr_yprs, ypr_cpr/
       | /4 width=1 by ypr_yprs, ypr_lpr, lpr_pair/
       ]
     ] -L1 -V1 -T20 -U2 /3 width=4/
@@ -115,7 +115,7 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
     elim (lift_total X 0 1) #W20 #H3
     lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1/ -H1 #HVW20
-    lapply (cpcs_lift (L2.ⓓW2) … H3 … HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
+    lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
     lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
     elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
     lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) [ /2 width=1/ ] -HW3 -HTU2 #HTU2
@@ -124,7 +124,7 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (IH1 … HT02 (L2.ⓓW2) ?) // [1,2: /2 width=1/ ] -L1 #HT2
     lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /2 width=1/ -HV0 -HV02 /3 width=8/
   ]
-| #W1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH2
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH2
   elim (snv_inv_cast … H1) -H1 #U1 #l #HW1 #HT1 #HTU1 #HUW1
   elim (cpr_inv_cast1 … H2) -H2
   [ * #W2 #T2 #HW12 #HT12 #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
index 3ba30937e..5a2fae488 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma
@@ -19,26 +19,26 @@ include "basic_2/dynamic/snv_cpcs.ma".
 
 (* Properties on stratified static type assignment for terms ****************)
 
-fact snv_ssta_aux: ∀h,g,L0,T0.
-                   (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                   (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                   (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                   ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ssta h g L1 T1.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*]
-[ #k #HL0 #HT0 #_ #X #l #H2 destruct -IH3 -IH2 -IH1
+fact snv_ssta_aux: ∀h,g,G0,L0,T0.
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                   ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_ssta h g G1 L1 T1.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [||||*]
+[ #k #HG0 #HL0 #HT0 #_ #X #l #H2 destruct -IH3 -IH2 -IH1
   elim (ssta_inv_sort1 … H2) -H2 #_ #H destruct //
-| #i #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
+| #i #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
   elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
   elim (ssta_inv_lref1 … H2) -H2 * #K0 #V0 #W1 [| #l ] #H #HVW1 #HX [| #_ ]
   lapply (ldrop_mono … H … HLK1) -H #H destruct
-  lapply (fsupp_lref … HLK1) #H
+  lapply (fsupp_lref … G1 … HLK1) #H
   lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=7/
-| #p #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 -IH1
+| #p #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
   elim (snv_inv_bind … H1) -H1 #HV1 #HT1
   elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=5/
-| #V1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct
   elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #HVW1 #HW10 #HT10
   elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
   lapply (IH1 … HT1 … HTU1) -IH1 /2 width=1/ #HU1
@@ -47,7 +47,7 @@ fact snv_ssta_aux: ∀h,g,L0,T0.
   elim (cpcs_inv_abst2 … HU0) -HU0 #W2 #U2 #HU2 #HU02
   elim (cprs_inv_abst … HU02) -HU02 #HW02 #_
   lapply (cprs_trans … HW10 … HW02) -W0 /3 width=10 by snv_appl, ex2_intro/ (**) (* auto is too slow without trace *)
-| #W1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2
   elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #HTU1 #HUW1
   lapply (ssta_inv_cast1 … H2) -H2 /3 width=5/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
index bb07981b0..28f87d7c4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma
@@ -20,21 +20,21 @@ include "basic_2/dynamic/lsubsv_ssta.ma".
 
 (* Properties on sn parallel reduction for local environments ***************)
 
-fact ssta_cpr_lpr_aux: ∀h,g,L0,T0.
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
-                       (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
-                       ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_cpr_lpr h g L1 T1.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *]
-[ #k #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1
+fact ssta_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+                       ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_ssta_cpr_lpr h g G1 L1 T1.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| *]
+[ #k #_ #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1
   elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct
   >(cpr_inv_sort1 … H3) -X3 /4 width=6/
-| #i #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+| #i #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
   elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1
   elim (ssta_inv_lref1 … H2) -H2 * #K1
   #V1 #W1 [| #l0 ] #HLK1 #HVW1 #HWU1 [| #H destruct ]
   lapply (ldrop_mono … H … HLK1) -H #H destruct
-  lapply (fsupp_lref … HLK1) #HKV1
+  lapply (fsupp_lref … G1 … HLK1) #HKV1
   elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
   elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
   lapply (ldrop_fwd_ldrop2 … HLK2) #H2
@@ -55,9 +55,9 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (ssta_lift … HVW2 … H2 … HW0 … HWU2) -HVW2 -HW0
     lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/
   ]
-| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
+| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
   elim (snv_inv_bind … H1) -H1 #_ #HT1
   elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
   elim (cpr_inv_bind1 … H3) -H3 *
@@ -70,7 +70,7 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (cpcs_bind1 true … V1 V1 … HU12) // -HU12 #HU12
     lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 /2 width=3/
   ]
-| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct
   elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10
   elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
   elim (cpr_inv_appl1 … H3) -H3 *
@@ -87,7 +87,7 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
     elim (ssta_cpcs_lpr_aux … IH2 IH1 … HWX1 … HWV22 … L1) -HWX1 //
     [2: /2 width=1/
-    |3: /4 width=4 by ygt_yprs_trans, fsupp_ygt, sstas_yprs, ssta_sstas/
+    |3: /4 width=5 by ygt_yprs_trans, fsupp_ygt, sstas_yprs, ssta_sstas/
     ] #H #_ destruct -X1
     lapply (IH2 … HV1 … HV12 … HL12) [ /2 width=1/ ] #HV2    
     lapply (IH2 … HW2 … HW20 … HL12) [ /2 width=1/ ] -IH2 #H2W20
@@ -117,7 +117,7 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0.
     lapply (cpcs_flat … HV10 … HU02 Appl) -HV10 -HU02 #HU02
     lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) [ /2 width=3/ ] -V0 /4 width=3/
   ]
-| #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+| #U0 #T1 #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
   elim (snv_inv_cast … H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_
   lapply (ssta_inv_cast1 … H2) -H2 #HTU1
   elim (ssta_mono … HT10 … HTU1) -HT10 #H1 #H2 destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma
index bc2d74497..da5a4c9cd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma
@@ -19,8 +19,8 @@ include "basic_2/dynamic/snv.ma".
 
 (* Forward_lemmas on iterated stratified static type assignment for terms ***)
 
-lemma snv_sstas_fwd_correct: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g] T2 →
+lemma snv_sstas_fwd_correct: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g] T2 →
                              ∃∃U2,l. ⦃G, L⦄ ⊢ T2 •[h, g] ⦃l, U2⦄.
-#h #g #L #T1 #T2 #HT1 #HT12
+#h #g #G #L #T1 #T2 #HT1 #HT12
 elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by sstas_fwd_correct/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
index 7b50bfdcf..0e4ed9f64 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma
@@ -12,67 +12,67 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/btpredstarproper_6.ma".
+include "basic_2/notation/relations/btpredstarproper_8.ma".
 include "basic_2/dynamic/ysc.ma".
 include "basic_2/dynamic/yprs.ma".
 
 (* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************)
 
-inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝
-| ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[h, g] ⦃L2, T2⦄ →
-            ygt h g L1 T1 L2 T2
-| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → ⦃G, L⦄ ⊢ ➡ L2 → ygt h g L1 T1 L2 T
+inductive ygt (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
+| ygt_inj : ∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+            ygt h g G1 L1 T1 G2 L2 T2
+| ygt_step: ∀G,L,L2,T. ygt h g G1 L1 T1 G L T → ⦃G, L⦄ ⊢ ➡ L2 → ygt h g G1 L1 T1 G L2 T
 .
 
 interpretation "'big tree' proper parallel computation (closure)"
-   'BTPRedStarProper h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2).
+   'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (ygt h g G1 L1 T1 G2 L2 T2).
 
 (* Basic forvard lemmas *****************************************************)
 
-lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄ →
-                    h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2
-/3 width=4 by yprs_strap1, ysc_ypr, ypr_lpr/
+lemma ygt_fwd_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ →
+                    ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2
+/3 width=5 by yprs_strap1, ysc_ypr, ypr_lpr/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma ysc_ygt: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[h, g] ⦃L2, T2⦄ →
-               h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄.
-/3 width=4/ qed.
+lemma ysc_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+               ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+/3 width=5/ qed.
 
-lemma ygt_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L, T⦄ →
-                  h ⊢ ⦃L, T⦄ ≽[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2
+lemma ygt_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
+                  ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ →  ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
 lapply (ygt_fwd_yprs … H1) #H0
-elim (ypr_inv_ysc … H2) -H2 [| * #HL2 #H destruct ] /2 width=4/
+elim (ypr_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] /2 width=5/
 qed-.
 
-lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L, T⦄ →
-                  h ⊢ ⦃L, T⦄ >[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -L2 -T2
-[ /3 width=4 by ygt_inj, yprs_strap2/ | /2 width=3/ ]
+lemma ygt_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
+                  ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2
+[ /3 width=5 by ygt_inj, yprs_strap2/ | /2 width=3/ ]
 qed-.
 
-lemma ygt_yprs_trans: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L, T⦄ →
-                      h ⊢ ⦃L, T⦄ ≥[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -L2 -T2 //
-/2 width=4 by ygt_strap1/
+lemma ygt_yprs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ →
+                      ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -G2 -L2 -T2 //
+/2 width=5 by ygt_strap1/
 qed-.
 
-lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ →
-                      ∀L2,T2. h ⊢ ⦃L, T⦄ >[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -L -T //
-/3 width=4 by ygt_strap2/
+lemma yprs_ygt_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+                      ∀G2,L2,T2. ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -G -L -T //
+/3 width=5 by ygt_strap2/
 qed-.
 
-lemma fsupp_ygt: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/
+lemma fsupp_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 /3 width=1/ /3 width=5/
 qed.
 
-lemma cprs_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
-                h ⊢ ⦃L, T1⦄ >[h, g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2
+lemma cprs_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
+                ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
+#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2
 [ #H elim H //
 | #T #T2 #_ #HT2 #IHT1 #HT12
   elim (term_eq_dec T1 T) #H destruct
@@ -83,9 +83,9 @@ lemma cprs_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥)
 ]
 qed.
 
-lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 → ⊥) →
-                 h ⊢ ⦃L, T1⦄ >[h, g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2
+lemma sstas_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 → ⊥) →
+                 ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
+#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2
 [ #H elim H //
 | #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12
   elim (term_eq_dec T1 T) #H destruct
@@ -96,6 +96,6 @@ lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 
 ]
 qed.
 
-lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) →
-                  h ⊢ ⦃L1, T⦄ >[h, g] ⦃L2, T⦄.
+lemma lsubsv_ygt: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) →
+                  ⦃G, L1, T⦄ >[h, g] ⦃G, L2, T⦄.
 /4 width=1/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma
index 99deeefb1..443dbcbf0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma
@@ -18,5 +18,5 @@ include "basic_2/dynamic/ygt.ma".
 
 (* Main properties **********************************************************)
 
-theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g).
-/3 width=4 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.
+theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g).
+/3 width=5 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
index 84879b10a..2c8c96d27 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma
@@ -12,26 +12,26 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/btpred_6.ma".
+include "basic_2/notation/relations/btpred_8.ma".
 include "basic_2/relocation/fsup.ma".
 include "basic_2/reduction/lpr.ma".
 include "basic_2/dynamic/lsubsv.ma".
 
 (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
 
-inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
-| ypr_fsup  : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2
-| ypr_lpr   : ∀L2. L1 ⊢ ➡ L2 → ypr h g L1 T1 L2 T1
-| ypr_cpr   : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
-| ypr_ssta  : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ypr h g L1 T1 L1 T2
-| ypr_lsubsv: ∀L2. h ⊢ L2 ¡⊑[h, g] L1 → ypr h g L1 T1 L2 T1
+inductive ypr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
+| ypr_fsup  : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2
+| ypr_lpr   : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1
+| ypr_cpr   : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2
+| ypr_ssta  : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ypr h g G1 L1 T1 G1 L1 T2
+| ypr_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → ypr h g G1 L1 T1 G1 L2 T1
 .
 
 interpretation
    "'big tree' parallel reduction (closure)"
-   'BTPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2).
+   'BTPRed h g G1 L1 T1 G2 L2 T2 = (ypr h g G1 L1 T1 G2 L2 T2).
 
 (* Basic properties *********************************************************)
 
-lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g).
+lemma ypr_refl: ∀h,g. tri_reflexive … (ypr h g).
 /2 width=1/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
index a8be72e72..c055f6040 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
@@ -12,71 +12,71 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/btpredstar_6.ma".
+include "basic_2/notation/relations/btpredstar_8.ma".
 include "basic_2/substitution/fsupp.ma".
 include "basic_2/computation/lprs.ma".
 include "basic_2/dynamic/ypr.ma".
 
 (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
 
-definition yprs: ∀h. sd h → bi_relation lenv term ≝
-                 λh,g. bi_TC … (ypr h g).
+definition yprs: ∀h. sd h → tri_relation genv lenv term ≝
+                 λh,g. tri_TC … (ypr h g).
 
 interpretation "'big tree' parallel computation (closure)"
-   'BTPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2).
+   'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (yprs h g G1 L1 T1 G2 L2 T2).
 
 (* Basic eliminators ********************************************************)
 
-lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 →
-                (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≽[h, g] ⦃L2, T2⦄ → R L T → R L2 T2) →
-                ∀L2,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄ → R L2 T2.
-/3 width=7 by bi_TC_star_ind/ qed-.
+lemma yprs_ind: ∀h,g,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 →
+                (∀L,G2,G,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+/3 width=8 by tri_TC_star_ind/ qed-.
 
-lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 →
-                   (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≥[h, g] ⦃L2, T2⦄ → R L T → R L1 T1) →
-                   ∀L1,T1. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄ → R L1 T1.
-/3 width=7 by bi_TC_star_ind_dx/ qed-.
+lemma yprs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 →
+                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
+                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1.
+/3 width=8 by tri_TC_star_ind_dx/ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g).
+lemma yprs_refl: ∀h,g. tri_reflexive … (yprs h g).
 /2 width=1/ qed.
 
-lemma ypr_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L2, T2⦄ →
-                h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄.
+lemma ypr_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+                ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 /2 width=1/ qed.
 
-lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ →
-                   h ⊢ ⦃L, T⦄ ≽[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄.
-/2 width=4/ qed-.
+lemma yprs_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+                   ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/2 width=5/ qed-.
 
-lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L, T⦄ →
-                   h ⊢ ⦃L, T⦄ ≥[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄.
-/2 width=4/ qed-.
+lemma yprs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
+                   ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/2 width=5/ qed-.
 
 (* Note: this is a general property of bi_TC *)
-lemma fsupp_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ →
-                  h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/
+lemma fsupp_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                  ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 /3 width=1/ /3 width=5/
 qed.
 
-lemma cprs_yprs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[h, g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/
+lemma cprs_yprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
+#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=5 by ypr_cpr, yprs_strap1/
 qed.
 
-lemma lprs_yprs: ∀h,g,L1,L2,T. L1 ⊢ ➡* L2 → h ⊢ ⦃L1, T⦄ ≥[h, g] ⦃L2, T⦄.
-#h #g #L1 #L2 #T #H @(lprs_ind … H) -L2 // /3 width=4 by ypr_lpr, yprs_strap1/
+lemma lprs_yprs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
+#h #g #G #L1 #L2 #T #H @(lprs_ind … H) -L2 // /3 width=5 by ypr_lpr, yprs_strap1/
 qed.
 
-lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 →
-                  h ⊢ ⦃L, T1⦄ ≥[h, g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/
+lemma sstas_yprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 →
+                  ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
+#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=5 by ypr_ssta, yprs_strap1/
 qed.
 
-lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[h, g] L1 → h ⊢ ⦃L1, T⦄ ≥[h, g] ⦃L2, T⦄.
+lemma lsubsv_yprs: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
 /3 width=1/ qed.
 
-lemma cprs_lpr_yprs: ∀h,g,L1,L2,T1,T2. L1 ⊢ T1 ➡* T2 → L1 ⊢ ➡ L2 →
-                     h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄.
-/3 width=4 by yprs_strap1, ypr_lpr, cprs_yprs/
+lemma cprs_lpr_yprs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
+                     ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄.
+/3 width=5 by yprs_strap1, ypr_lpr, cprs_yprs/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma
index 96354706d..d05f23c7c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma
@@ -16,5 +16,5 @@ include "basic_2/dynamic/yprs.ma".
 
 (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
 
-theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g).
-/2 width=4/ qed-.
+theorem yprs_trans: ∀h,g. tri_transitive … (yprs h g).
+/2 width=5/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
index 09785875c..2d4d80bc5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma
@@ -12,34 +12,35 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/notation/relations/btpredproper_6.ma".
+include "basic_2/notation/relations/btpredproper_8.ma".
 include "basic_2/dynamic/ypr.ma".
 
 (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
 
-inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝
-| ysc_fsup  : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ysc h g L1 T1 L2 T2
-| ysc_cpr   : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2
-| ysc_ssta  : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ysc h g L1 T1 L1 T2
-| ysc_lsubsv: ∀L2. h ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1
+inductive ysc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
+| ysc_fsup  : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ysc h g G1 L1 T1 G2 L2 T2
+| ysc_cpr   : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g G1 L1 T1 G1 L1 T2
+| ysc_ssta  : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ysc h g G1 L1 T1 G1 L1 T2
+| ysc_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → ysc h g G1 L1 T1 G1 L2 T1
 .
 
 interpretation
    "'big tree' proper parallel reduction (closure)"
-   'BTPRedProper h g L1 T1 L2 T2 = (ysc h g L1 T1 L2 T2).
+   'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (ysc h g G1 L1 T1 G2 L2 T2).
 
 (* Basic properties *********************************************************)
 
-lemma ysc_ypr: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[h, g] ⦃L2, T2⦄ →
-               h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /2 width=1/ /2 width=2/
+lemma ysc_ypr: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
+               ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1/ /2 width=2/
 qed.
 
 (* Inversion lemmas on "big tree" parallel reduction for closures ***********)
 
-lemma ypr_inv_ysc: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L2, T2⦄ →
-                   h ⊢ ⦃L1, T1⦄ ≻[h, g] ⦃L2, T2⦄ ∨ (L1 ⊢ ➡ L2 ∧ T1 = T2).
-#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /3 width=1/ /3 width=2/
+lemma ypr_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+                   ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ 
+                   ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡ L2 & T1 = T2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1/ /3 width=2/
 [ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/
 | #L2 #HL21 elim (lenv_eq_dec L1 L2) #H destruct /3 width=1/ /4 width=1/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
similarity index 83%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_6.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
index cfc3ae926..80e40a157 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRed $h $g $L1 $T1 $L2 $T2 }.
+   for @{ 'BTPRed $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
similarity index 82%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_6.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
index 60cc3ef50..bb6d3d1af 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRedStar $h $g $L1 $T1 $L2 $T2 }.
+   for @{ 'BTPRedProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
similarity index 82%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_6.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
index eaf9a0a79..3943a33fd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRedProper $h $g $L1 $T1 $L2 $T2 }.
+   for @{ 'BTPRedStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_8.ma
similarity index 82%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_6.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_8.ma
index b76e2a5d3..66d7a34ba 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ > break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRedStarProper $h $g $L1 $T1 $L2 $T2 }.
+   for @{ 'BTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
similarity index 88%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_4.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
index 5704d8ef9..a617f7923 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 g ] )"
+notation "hvbox( G ⊢ break term 46 L1 ¡ ⊑ break [ term 46 h, break term 46 g ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'NativeValid $h $g $L $T }.
+   for @{ 'LRSubEqV $h $g $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
similarity index 87%
rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_4.ma
rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
index 1124b8b8f..d6426f6c1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( h ⊢ break term 46 L1 ¡ ⊑ break [ term 46 g ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h, break term 46 g ] )"
    non associative with precedence 45
-   for @{ 'LRSubEqV $h $g $L1 $L2 }.
+   for @{ 'NativeValid $h $g $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index af73af5fc..76c69725f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -33,7 +33,7 @@
          Closure of context-sensitive extended computation
          for native validity.
    </news>
-   <news date="In progress.">
+   <news date="2013 August 7.">
          Passive support for global environments.
    </news>   
    <news date="2013 July 27.">
-- 
2.39.2