From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 27 Jul 2018 18:50:11 +0000 (+0200)
Subject: update in basic_2
X-Git-Tag: make_still_working~293
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29;p=helm.git

update in basic_2

+ refinement for native validity (lsubv)
  allows to prove cnv_cpm_trans_lpr_aux (rt-confluence implies validity)
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
new file mode 100644
index 000000000..2d9f53b9c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
@@ -0,0 +1,129 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpms_fpbg.ma".
+include "basic_2/rt_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
+include "basic_2/dynamic/cnv_drops.ma".
+include "basic_2/dynamic/cnv_etc.ma".
+include "basic_2/dynamic/lsubv_cnv.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with context-free parallel reduction for local environments *****)
+
+fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ →
+                           ∀G0,L0,T0.
+                           (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+                           (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+                           ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1.
+#a #h #o #Ha #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1
+  elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct //
+| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2
+  elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1
+  elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2
+  elim (lpr_inv_pair_sn … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (fqup_lref (Ⓣ) … G1 … HLK1) #HKL
+  elim (cpm_inv_lref1_drops … H2) -H2 *
+  [ #H1 #H2 destruct -HLK1 /4 width=7 by fqup_fpbg, cnv_lref_drops/
+  | #K0 #V0 #W0 #H #HVW0 #W0 -HV12
+    lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
+    lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
+  | #n #K0 #V0 #W0 #H #HVW0 #W0 #H destruct -HV12
+    lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
+    lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
+  ]
+| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 -IH1
+  elim (cnv_inv_gref … H1)
+| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2
+  elim (cnv_inv_bind … H1) -H1 #HV1 #HT1
+  elim (cpm_inv_bind1 … H2) -H2 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/
+  | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
+    /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/
+  ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
+  elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1
+  elim (cpm_inv_appl1 … H2) -H2 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+    lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+    elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
+    <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
+    elim (cnv_cpms_strip_lpr_far … IH2 … HTU1 … HT12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
+    #X #H #HTU2 -IH2 -IH1 -L1 -V1 -T1
+    elim (cpms_inv_abst_sn … H) -H #W2 #U2 #HW12 #_ #H destruct
+    elim (cprs_conf … HXW1 … HW12) -W1 #W1 #HXW1 #HW21
+    lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
+    lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
+    [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
+    @(cnv_appl … HV2W1 HTU2) // #H destruct
+  | #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
+    elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
+    elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
+    lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+    lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ #HW20
+    lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20
+    elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
+    <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
+    elim (cnv_cpms_strip_lpr_far … IH2 … HW130 … HW120 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW130 -HW120
+    <minus_n_O #XW30 #HXW30 #HW230 -IH2 -IH1 -L1 -V1 -W10 -T10
+    elim (cprs_conf … HXW1 … HXW30) -W30 #W30 #HXW1 #HXW30
+    lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W30
+    lapply (cprs_trans … HW230 … HXW30) -XW30 #HW230
+    /5 width=4 by lsubv_cnv_trans, lsubv_beta, cnv_cast, cnv_bind/
+  | #q #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct
+    elim (cnv_inv_bind … HT1) -HT1 #HW0 #HT0
+    elim (cpms_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+    elim (lifts_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
+    lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
+    lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0
+    lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ #HT2
+    elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV10 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV10
+    <minus_n_O <minus_O_n #XW1 #HXW1 #HXV0
+    elim (cnv_cpms_strip_lpr_far … IH2 … HTU0 … HT02 … (L2.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=2 by fqup_fpbg, lpr_pair/ ] -HTU0 -HT02 -HW02
+    #X #H #HTU2 -IH2 -IH1 -L1 -W0 -T0 -U1
+    elim (cpms_inv_abst_sn … H) -H #W #U2 #HW3 #_ #H destruct -U3
+    lapply (cnv_lifts … HV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -HV0 #HV2
+    elim (cpms_lifts_sn … HXV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -V0 #XW2 #HXW12 #HXVW2
+    lapply (cpms_lifts_bi … HXW1 (Ⓣ) … (L2.ⓓW2) … HW13 … HXW12) /3 width=1 by drops_refl, drops_drop/ -W1 -XW1 #HXW32
+    elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
+    lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
+    lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
+    @cnv_bind // @(cnv_appl … H1 H2) // #H destruct
+  ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
+  elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
+  elim (cpm_inv_cast1 … H2) -H2
+  [ * #W2 #T2 #HW12 #HT12 #H destruct
+    lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ #HW2
+    lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+    lapply (cnv_cpms_trans_lpr_far … IH1 … HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
+    elim (cnv_cpms_strip_lpr_far … IH2 … HWU1 … HW12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW12
+    <minus_n_O <minus_O_n #XW1 #HXUW1 #HXW21
+    elim (cnv_cpms_strip_lpr_far … IH2 … HTU1 … HT12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
+    #XT1 #HXUT1 #HXT21
+    elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
+    >eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1
+    lapply (cprs_trans … HXW21 … H1) -XW1 #H1
+    lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l #H2
+    /2 width=3 by cnv_cast/
+  | #HX -IH2 -HW1 -U1
+    lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
+  | * #n #HX #H destruct -IH2 -HT1 -U1
+    lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
index c2e0809f8..d7ac516cd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
@@ -48,16 +48,23 @@ definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
                                 ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
                                 ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
 
-(* Auxiliary properties for preservation ************************************)
+(* Properties for preservation **********************************************)
 
-fact cnv_cpms_trans_lpr_aux (a) (h) (o):
-                            ∀G0,L0,T0.
-                            (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
-                            ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+lemma cnv_cpms_trans_lpr_far (a) (h) (o):
+                             ∀G0,L0,T0.
+                             (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+                             ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
 #a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
 @(cpms_ind_dx … H) -n -T2
 /4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
 qed-.
+
+lemma cnv_cpms_strip_lpr_far (a) (h) (o):
+                             ∀G0,L0,T0.
+                             (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+                             ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
+
 (*
 fact cnv_cpms_strip_lpr_aux (a) (h) (o):
                             ∀G0,L0,T0.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma
deleted file mode 100644
index 4a87a4c3d..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpr.ma
+++ /dev/null
@@ -1,142 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/rt_computation/cpms_fpbg.ma".
-include "basic_2/rt_computation/cprs_cprs.ma".
-include "basic_2/rt_computation/lprs_cpms.ma".
-include "basic_2/dynamic/cnv_drops.ma".
-(*
-include "basic_2/dynamic/snv_aaa.ma".
-*)
-include "basic_2/dynamic/cnv_etc.ma".
-(*
-include "basic_2/dynamic/lsubsv_snv.ma".
-*)
-(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-
-(* Properties with context-free parallel reduction for local environments *****)
-
-fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ →
-                           ∀G0,L0,T0.
-                           (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
-                           (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
-                           ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1.
-#a #h #o #Ha #G0 #L0 #T0 (* #IH4 #IH3 *) #IH2 #IH1 #G1 #L1 * * [|||| * ]
-[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct (* -IH4 -IH3 *) -IH2 -IH1 -H1
-  elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct //
-| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2
-  elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1
-  elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2
-  elim (lpr_inv_pair_sn … H) -H #K2 #V2 #HK12 #HV12 #H destruct
-  lapply (fqup_lref (Ⓣ) … G1 … HLK1) #HKL
-  elim (cpm_inv_lref1_drops … H2) -H2 *
-  [ #H1 #H2 destruct -HLK1 /4 width=7 by fqup_fpbg, cnv_lref_drops/
-  | #K0 #V0 #W0 #H #HVW0 #W0 -HV12
-    lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
-    lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
-  | #n #K0 #V0 #W0 #H #HVW0 #W0 #H destruct -HV12
-    lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct
-    lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/
-  ]
-| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2 -IH1
-  elim (cnv_inv_gref … H1)
-| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 -IH3 *) -IH2
-  elim (cnv_inv_bind … H1) -H1 #HV1 #HT1
-  elim (cpm_inv_bind1 … H2) -H2 *
-  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/
-  | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
-    /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/
-  ]
-| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
-  elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1
-  elim (cpm_inv_appl1 … H2) -H2 *
-  [ #V2 #T2 #HV12 #HT12 #H destruct (* -IH4 *)
-    lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
-    lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
-    elim (IH2 … HVW1 … V2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12
-    <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
-    elim (IH2 … HTU1 … T2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HTU1 -HT12
-    #X #H #HTU2 (* -IH3 *) -IH2 -IH1 -L1 -V1 -T1
-    elim (cpms_inv_abst_sn … H) -H #W2 #U2 #HW12 #_ #H destruct
-    elim (cprs_conf … HXW1 … HW12) -W1 #W1 #HXW1 #HW21
-    lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
-    lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
-    [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
-    @(cnv_appl … HV2W1 HTU2) // #H destruct
-  | #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
-    elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
-    elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
-    lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
-    lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ #HW20
-    lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20
-    elim (IH2 … HVW1 … V2 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV12
-    <minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
-    elim (IH2 … HW130 … W20 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HW130 -HW120
-    <minus_n_O #XW30 #HXW30 #HW230
-    elim (cprs_conf … HXW1 … HXW30) -W30 #W30 #HXW1 #HXW30
-    lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W30
-    lapply (cprs_trans … HW230 … HXW30) -XW30 #HW230
-    @cnv_bind [ /2 width=3 by cnv_cast/ ]
-(*
-    @(lsubsv_snv_trans … HT20) -HT20
-    @(lsubsv_beta … (d-1)) //
-    @shnv_cast [1,2: // ] #d0 #Hd0
-    lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20d … HV2d … d0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20d -HV2d -HVW20
-    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/
-*)
-  | #q #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct (* -IH4 *)
-    elim (cnv_inv_bind … HT1) -HT1 #HW0 #HT0
-    elim (cpms_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
-    elim (lifts_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
-    lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
-    lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0
-    lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ #HT2
-    elim (IH2 … HVW1 … V0 … L2 … L2) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HVW1 -HV10
-    <minus_n_O <minus_O_n #XW1 #HXW1 #HXV0
-    elim (IH2 … HTU0 … T2 … (L2.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=2 by fqup_fpbg, cpm_cpms, lpr_pair/ ] -HT02 -HTU0 -HW02
-    #X #H #HTU2 -IH2 -IH1
-    elim (cpms_inv_abst_sn … H) -H #W #U2 #HW3 #_ #H destruct -U3
-    lapply (cnv_lifts … HV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -HV0 #HV2
-    elim (cpms_lifts_sn … HXV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -V0 #XW2 #HXW12 #HXVW2
-    lapply (cpms_lifts_bi … HXW1 (Ⓣ) … (L2.ⓓW2) … HW13 … HXW12) /3 width=1 by drops_refl, drops_drop/ -W1 -XW1 #HXW32
-    elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
-    lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
-    lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
-    @cnv_bind // @(cnv_appl … H1 H2) // #H destruct 
-  ]
-| #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct (* -IH4 *)
-  elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
-  elim (cpm_inv_cast1 … H2) -H2
-  [ * #W2 #T2 #HW12 #HT12 #H destruct
-    lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ #HW2
-    lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
-    lapply (cnv_cpms_trans_lpr_aux … IH1 … HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
-    elim (IH2 … HWU1 … W2 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HW12
-    <minus_n_O <minus_O_n #XW1 #HXUW1 #HXW21
-    elim (IH2 … HTU1 … T2 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg, cpm_cpms/ ] -HTU1 -HT12
-    #XT1 #HXUT1 #HXT21
-    elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
-    >eq_minus_O // #W0 #H1 #H2
-    lapply (cprs_trans … HXW21 … H1) -XW1 #H1
-    lapply (cpms_trans … HXT21 … H2) -XT1 <arith_l #H2
-    /2 width=3 by cnv_cast/
-  | #HX (* -IH3 *) -IH2 -HW1 -U1
-    lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
-  | * #n #HX #H destruct -IH2 -HT1 -U1
-    lapply (IH1 … HX … HL12) /2 width=1 by fqup_fpbg/
-  ]
-]
-(*
-qed-.
-*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
deleted file mode 100644
index 9fe022334..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma
+++ /dev/null
@@ -1,161 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/lrsubeqv_5.ma".
-include "basic_2/dynamic/shnv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Note: this is not transitive *)
-inductive lsubsv (h) (o) (G): relation lenv ≝
-| lsubsv_atom: lsubsv h o G (⋆) (⋆)
-| lsubsv_pair: ∀I,L1,L2,V. lsubsv h o G L1 L2 →
-               lsubsv h o G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubsv_beta: ∀L1,L2,W,V,d1. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, o, d1] → ⦃G, L2⦄ ⊢ W ¡[h, o] →
-               ⦃G, L1⦄ ⊢ V ▪[h, o] d1+1 → ⦃G, L2⦄ ⊢ W ▪[h, o] d1 →
-               lsubsv h o G L1 L2 → lsubsv h o G (L1.ⓓⓝW.V) (L2.ⓛW)
-.
-
-interpretation
-  "local environment refinement (stratified native validity)"
-  'LRSubEqV h o G L1 L2 = (lsubsv h o G L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubsv_inv_atom1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 = ⋆ → L2 = ⋆.
-#h #o #G #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubsv_inv_atom1: ∀h,o,G,L2. G ⊢ ⋆ ⫃¡[h, o] L2 → L2 = ⋆.
-/2 width=6 by lsubsv_inv_atom1_aux/ qed-.
-
-fact lsubsv_inv_pair1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
-                           ∀I,K1,X. L1 = K1.ⓑ{I}X →
-                           (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
-                           ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
-                                       ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
-                                        G ⊢ K1 ⫃¡[h, o] K2 &
-                                        I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-#h #o #G #L1 #L2 * -L1 -L2
-[ #J #K1 #X #H destruct
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K1 #X #H destruct /3 width=11 by or_intror, ex8_4_intro/
-]
-qed-.
-
-lemma lsubsv_inv_pair1: ∀h,o,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃¡[h, o] L2 →
-                        (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
-                        ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
-                                     ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
-                                     G ⊢ K1 ⫃¡[h, o] K2 &
-                                     I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
-
-fact lsubsv_inv_atom2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L2 = ⋆ → L1 = ⋆.
-#h #o #G #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubsv_inv_atom2: ∀h,o,G,L1. G ⊢ L1 ⫃¡[h, o] ⋆ → L1 = ⋆.
-/2 width=6 by lsubsv_inv_atom2_aux/ qed-.
-
-fact lsubsv_inv_pair2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
-                           ∀I,K2,W. L2 = K2.ⓑ{I}W →
-                           (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
-                           ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
-                                      ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
-                                      G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
-#h #o #G #L1 #L2 * -L1 -L2
-[ #J #K2 #U #H destruct
-| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K2 #U #H destruct /3 width=8 by or_intror, ex7_3_intro/
-]
-qed-.
-
-lemma lsubsv_inv_pair2: ∀h,o,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, o] K2.ⓑ{I}W →
-                        (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
-                        ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
-                                   ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
-                                   G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
-/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsubsv_fwd_lsubr: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 ⫃ L2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsubsv_refl: ∀h,o,G,L. G ⊢ L ⫃¡[h, o] L.
-#h #o #G #L elim L -L /2 width=1 by lsubsv_pair/
-qed.
-
-lemma lsubsv_cprs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
-                         ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2.
-/3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
-qed-.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_drop_O1_conf: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
-                           ∀K1,b,k. ⬇[b, 0, k] L1 ≘ K1 →
-                           ∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L2 ≘ K2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #b #k #H
-  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
-  [ destruct
-    elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
-    <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
-  | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
-  ]
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K1 #b #k #H
-  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
-  [ destruct
-    elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
-    <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
-  | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
-  ]
-]
-qed-.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_drop_O1_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
-                            ∀K2,b, k. ⬇[b, 0, k] L2 ≘ K2 →
-                            ∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L1 ≘ K1.
-#h #o #G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #b #k #H
-  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
-  [ destruct
-    elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
-    <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
-  | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
-  ]
-| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K2 #b #k #H
-  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
-  [ destruct
-    elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
-    <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
-  | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
-  ]
-]
-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
deleted file mode 100644
index 01d320772..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma
+++ /dev/null
@@ -1,25 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties on context-sensitive parallel equivalence for terms ***********)
-
-lemma lsubsv_cpcs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] 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_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma
deleted file mode 100644
index fa1b25fea..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma
+++ /dev/null
@@ -1,98 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/equivalence/scpes_cpcs.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties on nat-iterated static type assignment ************************)
-
-lemma lsubsv_lstas_trans: ∀h,o,G,L2,T,U2,d2. ⦃G, L2⦄ ⊢ T •*[h, d2] U2 →
-                          ∀d1. d2 ≤ d1 → ⦃G, L2⦄ ⊢ T ▪[h, o] d1 →
-                          ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
-                          ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, d2] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
-#h #o #G #L2 #T #U #d2 #H elim H -G -L2 -T -U -d2
-[ /2 width=3 by ex2_intro/
-| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
-  elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0
-  lapply (drop_mono … HK0 … HLK2) -HK0 #H destruct
-  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
-  elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HWU -IHVW -HLK1 ]
-  [ #HK12 #H destruct
-    elim (IHVW … Hd21 HV0 … HK12) -K2 -d1 #T #HVT #HTW
-    lapply (drop_fwd_drop2 … HLK1) #H
-    elim (lift_total T 0 (i+1))
-    /3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/
-  | #V0 #d0 #_ #_ #_ #_ #_ #H destruct
-  ]
-| #G #L2 #K2 #V #W #i #HLK2 #_ #IHVW #d1 #_ #Hd1 #L1 #HL12
-  elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
-  lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
-  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
-  elim (lsubsv_inv_pair2 … H) -H * #K1
-  [ #HK12 #H destruct
-    elim (IHVW … HV0 … HK12) -K2 /3 width=5 by lstas_zero, ex2_intro/
-  | #V1 #d1 #_ #_ #HV1 #HV #HK12 #_ #H destruct
-    lapply (da_mono … HV0 … HV) -HV #H destruct
-    elim (da_lstas … HV1 0) -HV1 #W1 #HVW1 #_
-    elim (lift_total W1 0 (i+1)) #U1 #HWU1
-    elim (IHVW … HV0 … HK12) -K2 // #X #HVX #_ -W
-    @(ex2_intro … U1) /3 width=6 by lstas_cast, lstas_ldef/ (**) (* full auto too slow *)
-    @cpcs_cprs_sn @(cprs_delta … HLK1 … HWU1)
-    /4 width=2 by cprs_strap1, cpr_cprs, lstas_cpr, cpr_eps/
-  ]
-| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
-  elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
-  lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
-  lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21
-  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
-  elim (lsubsv_inv_pair2 … H) -H * #K1
-  [ #HK12 #H destruct
-    elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X
-    lapply (drop_fwd_drop2 … HLK1)
-    elim (lift_total X 0 (i+1))
-    /3 width=12 by lstas_succ, cpcs_lift, ex2_intro/
-  | #V1 #d1 #H0 #_ #HV1 #HV #HK12 #_ #H destruct
-    lapply (da_mono … HV0 … HV) -HV #H destruct
-    elim (shnv_inv_cast … H0) -H0 #_ #_ #H
-    lapply (H … Hd21) -H #HVV1
-    elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X #HVX #HXW
-    elim (da_lstas … HV1 (d2+1)) -HV1 #X1 #HVX1 #_
-    lapply (scpes_inv_lstas_eq … HVV1 … HVX … HVX1) -HVV1 -HVX #HXX1
-    lapply (cpcs_canc_sn … HXX1 … HXW) -X
-    elim (lift_total X1 0 (i+1))
-    lapply (drop_fwd_drop2 … HLK1)
-    /4 width=12 by cpcs_lift, lstas_cast, lstas_ldef, ex2_intro/
-  ]
-| #a #I #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
-  lapply (da_inv_bind … Hd2) -Hd2 #Hd2
-  elim (IHTU2 … Hd2 (L1.ⓑ{I}V2) …)
-  /3 width=3 by lsubsv_pair, lstas_bind, cpcs_bind_dx, ex2_intro/
-| #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
-  lapply (da_inv_flat … Hd2) -Hd2 #Hd2
-  elim (IHTU2 … Hd2 … HL12) -L2
-  /3 width=5 by lstas_appl, cpcs_flat, ex2_intro/
-| #G #L2 #W2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
-  lapply (da_inv_flat … Hd2) -Hd2 #Hd2
-  elim (IHTU2 … Hd2 … HL12) -L2
-  /3 width=3 by lstas_cast, ex2_intro/
-]
-qed-.
-
-lemma lsubsv_sta_trans: ∀h,o,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •*[h, 1] U2 →
-                        ∀d. ⦃G, L2⦄ ⊢ T ▪[h, o] d+1 →
-                        ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
-                        ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, 1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
-/2 width=7 by lsubsv_lstas_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
deleted file mode 100644
index 51d490222..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/equivalence/scpes_aaa.ma".
-include "basic_2/dynamic/snv_aaa.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Forward lemmas on lenv refinement for atomic arity assignment ************)
-
-lemma lsubsv_fwd_lsuba: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃⁝ L2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_pair/
-#L1 #L2 #W #V #d1 #H #_ #_ #_ #_ #IHL12
-elim (shnv_inv_cast … H) -H #HW #HV #H
-lapply (H 0 ?) // -d1 #HWV
-elim (snv_fwd_aaa … HW) -HW #B #HW
-elim (snv_fwd_aaa … HV) -HV #A #HV
-lapply (scpes_aaa_mono … HWV … HW … HV) #H destruct
-/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma
deleted file mode 100644
index 7f9e72946..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "static_2/static/lsubd.ma".
-include "basic_2/dynamic/lsubsv.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Forward lemmas on lenv refinement for degree assignment ******************)
-
-lemma lsubsv_fwd_lsubd: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃▪[h, o] L2.
-#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=3 by lsubd_pair, lsubd_beta/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma
deleted file mode 100644
index cac43d361..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_scpds.ma
+++ /dev/null
@@ -1,32 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "static_2/static/lsubd_da.ma".
-include "basic_2/dynamic/lsubsv_lsubd.ma".
-include "basic_2/dynamic/lsubsv_lstas.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties on decomposed extended parallel computation on terms **********)
-
-lemma lsubsv_scpds_trans: ∀h,o,G,L2,T1,T2,d. ⦃G, L2⦄ ⊢ T1 •*➡*[h, o, d] T2 →
-                          ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
-                          ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
-#h #o #G #L2 #T1 #T2 #d2 * #T #d1 #Hd21 #Hd1 #HT1 #HT2 #L1 #HL12
-lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
-elim (lsubsv_lstas_trans … HT1 … Hd1 … HL12) // #T0 #HT10 #HT0
-lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02
-elim (cpcs_inv_cprs … HT02) -HT02
-/5 width=5 by lsubsv_fwd_lsubd, lsubd_da_trans, ex4_2_intro, ex2_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
deleted file mode 100644
index 365849c36..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma
+++ /dev/null
@@ -1,44 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/dynamic/lsubsv_scpds.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-
-(* Properties concerning stratified native validity *************************)
-
-lemma lsubsv_snv_trans: ∀h,o,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, o] →
-                        ∀L1. G ⊢ L1 ⫃¡[h, o] L2 → ⦃G, L1⦄ ⊢ T ¡[h, o].
-#h #o #G #L2 #T #H elim H -G -L2 -T //
-[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12
-  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
-  elim (lsubsv_inv_pair2 … H) -H * #K1
-  [ #HK12 #H destruct /3 width=5 by snv_lref/
-  | #W #d #HVW #_ #_ #_ #_ #H1 #H2 destruct -IHV
-    /3 width=6 by shnv_inv_snv, snv_lref/
-  ]
-| #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct
-  /4 width=1 by snv_bind, lsubsv_pair/
-| #a #G #L2 #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 #IHV #IHT #L1 #HL12
-  elim (lsubsv_scpds_trans … HVW0 … HL12) -HVW0 #V0 #HV0 #HWV0
-  elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X #HT0 #H
-  elim (cprs_inv_abst1 … H) -H #W #T0 #HW0 #_ #H destruct
-  elim (cprs_conf … HWV0 … HW0) -W0
-  /4 width=10 by snv_appl, scpds_cprs_trans, cprs_bind/
-| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
-  elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X0 #HTX0 #H1
-  elim (lsubsv_scpds_trans … HU0 … HL12) -HU0 #X #HUX #H2
-  elim (cprs_conf … H1 … H2) -U0 /3 width=5 by snv_cast, scpds_cprs_trans/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
new file mode 100644
index 000000000..bba857ac8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
@@ -0,0 +1,103 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/lrsubeqv_5.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Note: this is not transitive *)
+inductive lsubv (a) (h) (G): relation lenv ≝
+| lsubv_atom: lsubv a h G (⋆) (⋆)
+| lsubv_bind: ∀I,L1,L2. lsubv a h G L1 L2 → lsubv a h G (L1.ⓘ{I}) (L2.ⓘ{I})
+| lsubv_beta: ∀L1,L2,W,V. ⦃G, L1⦄ ⊢ ⓝW.V ![a,h] → ⦃G, L2⦄ ⊢ W ![a,h] →
+              lsubv a h G L1 L2 → lsubv a h G (L1.ⓓⓝW.V) (L2.ⓛW)
+.
+
+interpretation
+  "local environment refinement (native validity)"
+  'LRSubEqV a h G L1 L2 = (lsubv a h G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 = ⋆ → L2 = ⋆.
+#a #h #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_atom1 *)
+lemma lsubv_inv_atom_sn (a) (h) (G): ∀L2. G ⊢ ⋆ ⫃![a,h] L2 → L2 = ⋆.
+/2 width=6 by lsubv_inv_atom_sn_aux/ qed-.
+
+fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+                           ∀I,K1. L1 = K1.ⓘ{I} →
+                           ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
+                            | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                                        G ⊢ K1 ⫃![a,h] K2 &
+                                        I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+#a #h #G #L1 #L2 * -L1 -L2
+[ #J #K1 #H destruct
+| #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #HWV #HW #HL12 #J #K1 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_pair1 *)
+lemma lsubv_inv_bind_sn (a) (h) (G): ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 →
+                        ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
+                         | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                                     G ⊢ K1 ⫃![a,h] K2 &
+                                     I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+/2 width=3 by lsubv_inv_bind_sn_aux/ qed-.
+
+fact lsubv_inv_atom_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 = ⋆ → L1 = ⋆.
+#a #h #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_atom2 *)
+lemma lsubv_inv_atom2 (a) (h) (G): ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆.
+/2 width=6 by lsubv_inv_atom_dx_aux/ qed-.
+
+fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+                           ∀I,K2. L2 = K2.ⓘ{I} →
+                           ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
+                            | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                                        G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
+#a #h #G #L1 #L2 * -L1 -L2
+[ #J #K2 #H destruct
+| #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #HWV #HW #HL12 #J #K2 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+]
+qed-.
+
+(* Basic_2A1: uses: lsubsv_inv_pair2 *)
+lemma lsubv_inv_bind_dx (a) (h) (G): ∀I,L1,K2. G ⊢ L1 ⫃![a,h] K2.ⓘ{I} →
+                        ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
+                         | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                                     G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
+/2 width=3 by lsubv_inv_bind_dx_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: uses: lsubsv_refl *)
+lemma lsubv_refl (a) (h) (G): reflexive … (lsubv a h G).
+#a #h #G #L elim L -L /2 width=1 by lsubv_atom, lsubv_bind/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma
new file mode 100644
index 000000000..b1782a021
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cnv.ma
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/dynamic/lsubv_cpms.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with native validity **************************************)
+
+(* Basic_2A1: uses: lsubsv_snv_trans *)
+lemma lsubv_cnv_trans (a) (h) (G):
+                      ∀L2,T. ⦃G, L2⦄ ⊢ T ![a,h] →
+                      ∀L1. G ⊢ L1 ⫃![a,h] L2 → ⦃G, L1⦄ ⊢ T ![a,h].
+#a #h #G #L2 #T #H elim H -G -L2 -T //
+[ #I #G #K2 #V #HV #IH #L1 #H
+  elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_zero/
+| #I #G #K2 #i #_ #IH #L1 #H
+  elim (lsubv_inv_bind_dx … H) -H * /3 width=1 by cnv_lref/
+| #p #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12
+  /4 width=1 by cnv_bind, lsubv_bind/
+| #n #p #G #L2 #V #W #T #U #Ha #_ #_ #HVW #HTU #IHV #IHT #L1 #HL
+  /4 width=10 by lsubv_cpms_trans, cnv_appl/
+| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
+  /4 width=6 by lsubv_cpms_trans, cnv_cast/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
new file mode 100644
index 000000000..c02ec80b0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpcs.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_equivalence/cpcs_lsubr.ma".
+include "basic_2/dynamic/lsubv_lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with context-sensitive r-equivalence for terms ************)
+
+(* Basic_2A1: uses: lsubsv_cprs_trans *)
+lemma lsubv_cpcs_trans (a) (h) (G): lsub_trans … (cpcs h G) (lsubv a h G).
+/3 width=6 by lsubv_fwd_lsubr, lsubr_cpcs_trans/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
new file mode 100644
index 000000000..81d385add
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_cpms.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpms_lsubr.ma".
+include "basic_2/dynamic/lsubv_lsubr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with t-bound contex-sensitive rt-computation for terms ****)
+
+(* Basic_2A1: uses: lsubsv_cprs_trans lsubsv_scpds_trans *)
+lemma lsubv_cpms_trans (a) (n) (h) (G): lsub_trans … (λL. cpms h G L n) (lsubv a h G).
+/3 width=6 by lsubv_fwd_lsubr, lsubr_cpms_trans/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
new file mode 100644
index 000000000..90b59cba0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "static_2/relocation/drops.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_2A1: includes: lsubsv_drop_O1_conf *)
+lemma lsubv_drops_conf_isuni (a) (h) (G):
+                             ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+                             ∀b,f,K1. 𝐔⦃f⦄ → ⬇*[b,f] L1 ≘ K1 →
+                             ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L2 ≘ K2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H
+  elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
+  | #g #Hg #HLK1 #H destruct -HL12
+    elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+| #L1 #L2 #W #V #HVW #HW #HL12 #IH #b #f #K1 #Hf #H
+  elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
+  | #g #Hg #HLK1 #H destruct -HL12
+    elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+]
+qed-.
+
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_2A1: includes: lsubsv_drop_O1_trans *)
+lemma lsubv_drops_trans_isuni (a) (h) (G):
+                              ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
+                              ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2 →
+                              ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L1 ≘ K1.
+#a #h #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H
+  elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
+  | #g #Hg #HLK2 #H destruct -HL12
+    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+| #L1 #L2 #W #V #HWV #HW #HL12 #IH #b #f #K2 #Hf #H
+  elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
+  | #g #Hg #HLK2 #H destruct -HL12
+    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
new file mode 100644
index 000000000..ac03aa297
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/dynamic/cnv_aaa.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with lenv refinement for atomic arity assignment **********)
+
+(* Basic_2A1: uses: lsubsv_fwd_lsuba *)
+lemma lsubsv_fwd_lsuba (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → G ⊢ L1 ⫃⁝ L2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_bind/
+#L1 #L2 #W #V #H #_ #_ #IH
+elim (cnv_inv_cast … H) -H #W0 #HW #HV #HW0 #HVW0
+elim (cnv_fwd_aaa … HW) -HW #B #HW
+elim (cnv_fwd_aaa … HV) -HV #A #HV
+lapply (cpms_aaa_conf … HW … HW0) -HW0 #H
+lapply (cpms_aaa_conf … HV … HVW0) -HVW0 #HW0
+lapply (aaa_mono … H … HW0) -W0 #H destruct
+/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma
new file mode 100644
index 000000000..938c116c5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubr.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "static_2/static/lsubr.ma".
+include "basic_2/dynamic/lsubv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Forward lemmas with restricted refinement for local environments *********)
+
+(* Basic_2A1: uses: lsubsv_fwd_lsubr *)
+lemma lsubv_fwd_lsubr (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 ⫃ L2.
+#a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_beta/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
index 87d2cd592..ad9b95be0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
@@ -1,2 +1,3 @@
 cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma
-cnv_etc.ma cnv_lpr.ma
+cnv_etc.ma cnv_cpm_trans.ma
+lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma
deleted file mode 100644
index 961643418..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/shnv.ma
+++ /dev/null
@@ -1,55 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/notation/relations/nativevalid_6.ma".
-include "basic_2/equivalence/scpes.ma".
-include "basic_2/dynamic/snv.ma".
-
-(* STRATIFIED HIGHER NATIVE VALIDITY FOR TERMS ******************************)
-
-inductive shnv (h) (o) (d1) (G) (L): predicate term ≝
-| shnv_cast: ∀U,T. ⦃G, L⦄ ⊢ U ¡[h, o] → ⦃G, L⦄ ⊢ T ¡[h, o] →
-             (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T) →
-             shnv h o d1 G L (ⓝU.T)
-.
-
-interpretation "stratified higher native validity (term)"
-   'NativeValid h o d G L T = (shnv h o d G L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact shnv_inv_cast_aux: ∀h,o,G,L,X,d1. ⦃G, L⦄ ⊢ X ¡[h, o, d1] → ∀U,T. X = ⓝU.T →
-                        ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
-                         & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
-#h #o #G #L #X #d1 * -X
-#U #T #HU #HT #HUT #U1 #T1 #H destruct /3 width=1 by and3_intro/
-qed-.
-
-lemma shnv_inv_cast: ∀h,o,G,L,U,T,d1. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, d1] →
-                     ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
-                      & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
-/2 width=3 by shnv_inv_cast_aux/ qed-.
-
-lemma shnv_inv_snv: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ¡[h, o, d] → ⦃G, L⦄ ⊢ T ¡[h, o].
-#h #o #G #L #T #d * -T
-#U #T #HU #HT #HUT elim (HUT 0) -HUT /2 width=3 by snv_cast/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma snv_shnv_cast: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, 0].
-#h #o #G #L #U #T #H elim (snv_inv_cast … H) -H
-#U0 #HU #HT #HU0 #HTU0 @shnv_cast // -HU -HT
-#d #H <(le_n_O_to_eq … H) -d /2 width=3 by scpds_div/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc
new file mode 100644
index 000000000..9fe022334
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc
@@ -0,0 +1,161 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/lrsubeqv_5.ma".
+include "basic_2/dynamic/shnv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Note: this is not transitive *)
+inductive lsubsv (h) (o) (G): relation lenv ≝
+| lsubsv_atom: lsubsv h o G (⋆) (⋆)
+| lsubsv_pair: ∀I,L1,L2,V. lsubsv h o G L1 L2 →
+               lsubsv h o G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubsv_beta: ∀L1,L2,W,V,d1. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, o, d1] → ⦃G, L2⦄ ⊢ W ¡[h, o] →
+               ⦃G, L1⦄ ⊢ V ▪[h, o] d1+1 → ⦃G, L2⦄ ⊢ W ▪[h, o] d1 →
+               lsubsv h o G L1 L2 → lsubsv h o G (L1.ⓓⓝW.V) (L2.ⓛW)
+.
+
+interpretation
+  "local environment refinement (stratified native validity)"
+  'LRSubEqV h o G L1 L2 = (lsubsv h o G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubsv_inv_atom1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 = ⋆ → L2 = ⋆.
+#h #o #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsv_inv_atom1: ∀h,o,G,L2. G ⊢ ⋆ ⫃¡[h, o] L2 → L2 = ⋆.
+/2 width=6 by lsubsv_inv_atom1_aux/ qed-.
+
+fact lsubsv_inv_pair1_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+                           ∀I,K1,X. L1 = K1.ⓑ{I}X →
+                           (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
+                           ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+                                       ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+                                        G ⊢ K1 ⫃¡[h, o] K2 &
+                                        I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+#h #o #G #L1 #L2 * -L1 -L2
+[ #J #K1 #X #H destruct
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K1 #X #H destruct /3 width=11 by or_intror, ex8_4_intro/
+]
+qed-.
+
+lemma lsubsv_inv_pair1: ∀h,o,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃¡[h, o] L2 →
+                        (∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & L2 = K2.ⓑ{I}X) ∨
+                        ∃∃K2,W,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+                                     ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+                                     G ⊢ K1 ⫃¡[h, o] K2 &
+                                     I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
+
+fact lsubsv_inv_atom2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L2 = ⋆ → L1 = ⋆.
+#h #o #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #W #V #d1 #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubsv_inv_atom2: ∀h,o,G,L1. G ⊢ L1 ⫃¡[h, o] ⋆ → L1 = ⋆.
+/2 width=6 by lsubsv_inv_atom2_aux/ qed-.
+
+fact lsubsv_inv_pair2_aux: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+                           ∀I,K2,W. L2 = K2.ⓑ{I}W →
+                           (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
+                           ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+                                      ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+                                      G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
+#h #o #G #L1 #L2 * -L1 -L2
+[ #J #K2 #U #H destruct
+| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #HL12 #J #K2 #U #H destruct /3 width=8 by or_intror, ex7_3_intro/
+]
+qed-.
+
+lemma lsubsv_inv_pair2: ∀h,o,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, o] K2.ⓑ{I}W →
+                        (∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & L1 = K1.ⓑ{I}W) ∨
+                        ∃∃K1,V,d1. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, o, d1] & ⦃G, K2⦄ ⊢ W ¡[h, o] &
+                                   ⦃G, K1⦄ ⊢ V ▪[h, o] d1+1 & ⦃G, K2⦄ ⊢ W ▪[h, o] d1 &
+                                   G ⊢ K1 ⫃¡[h, o] K2 & I = Abst & L1 = K1.ⓓⓝW.V.
+/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubsv_fwd_lsubr: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → L1 ⫃ L2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubsv_refl: ∀h,o,G,L. G ⊢ L ⫃¡[h, o] L.
+#h #o #G #L elim L -L /2 width=1 by lsubsv_pair/
+qed.
+
+lemma lsubsv_cprs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+                         ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2.
+/3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
+qed-.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsv_drop_O1_conf: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+                           ∀K1,b,k. ⬇[b, 0, k] L1 ≘ K1 →
+                           ∃∃K2. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L2 ≘ K2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #b #k #H
+  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
+  [ destruct
+    elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
+    <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
+  | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+  ]
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K1 #b #k #H
+  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
+  [ destruct
+    elim (IHL12 L1 b 0) -IHL12 // #X #HL12 #H
+    <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
+  | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+  ]
+]
+qed-.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubsv_drop_O1_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 →
+                            ∀K2,b, k. ⬇[b, 0, k] L2 ≘ K2 →
+                            ∃∃K1. G ⊢ K1 ⫃¡[h, o] K2 & ⬇[b, 0, k] L1 ≘ K1.
+#h #o #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #b #k #H
+  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
+  [ destruct
+    elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
+    <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, drop_pair, ex2_intro/
+  | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+  ]
+| #L1 #L2 #W #V #d1 #HWV #HW #HVd1 #HWd1 #_ #IHL12 #K2 #b #k #H
+  elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
+  [ destruct
+    elim (IHL12 L2 b 0) -IHL12 // #X #HL12 #H
+    <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
+  | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc
new file mode 100644
index 000000000..01d320772
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_cpcs.etc
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on context-sensitive parallel equivalence for terms ***********)
+
+lemma lsubsv_cpcs_trans: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] 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/etc/lsubsv/lsubsv_lstas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lstas.etc
new file mode 100644
index 000000000..fa1b25fea
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lstas.etc
@@ -0,0 +1,98 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/scpes_cpcs.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on nat-iterated static type assignment ************************)
+
+lemma lsubsv_lstas_trans: ∀h,o,G,L2,T,U2,d2. ⦃G, L2⦄ ⊢ T •*[h, d2] U2 →
+                          ∀d1. d2 ≤ d1 → ⦃G, L2⦄ ⊢ T ▪[h, o] d1 →
+                          ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
+                          ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, d2] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
+#h #o #G #L2 #T #U #d2 #H elim H -G -L2 -T -U -d2
+[ /2 width=3 by ex2_intro/
+| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
+  elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0
+  lapply (drop_mono … HK0 … HLK2) -HK0 #H destruct
+  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
+  elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HWU -IHVW -HLK1 ]
+  [ #HK12 #H destruct
+    elim (IHVW … Hd21 HV0 … HK12) -K2 -d1 #T #HVT #HTW
+    lapply (drop_fwd_drop2 … HLK1) #H
+    elim (lift_total T 0 (i+1))
+    /3 width=12 by lstas_ldef, cpcs_lift, ex2_intro/
+  | #V0 #d0 #_ #_ #_ #_ #_ #H destruct
+  ]
+| #G #L2 #K2 #V #W #i #HLK2 #_ #IHVW #d1 #_ #Hd1 #L1 #HL12
+  elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
+  lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
+  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
+  elim (lsubsv_inv_pair2 … H) -H * #K1
+  [ #HK12 #H destruct
+    elim (IHVW … HV0 … HK12) -K2 /3 width=5 by lstas_zero, ex2_intro/
+  | #V1 #d1 #_ #_ #HV1 #HV #HK12 #_ #H destruct
+    lapply (da_mono … HV0 … HV) -HV #H destruct
+    elim (da_lstas … HV1 0) -HV1 #W1 #HVW1 #_
+    elim (lift_total W1 0 (i+1)) #U1 #HWU1
+    elim (IHVW … HV0 … HK12) -K2 // #X #HVX #_ -W
+    @(ex2_intro … U1) /3 width=6 by lstas_cast, lstas_ldef/ (**) (* full auto too slow *)
+    @cpcs_cprs_sn @(cprs_delta … HLK1 … HWU1)
+    /4 width=2 by cprs_strap1, cpr_cprs, lstas_cpr, cpr_eps/
+  ]
+| #G #L2 #K2 #V #W #U #i #d2 #HLK2 #_ #HWU #IHVW #d1 #Hd21 #Hd1 #L1 #HL12
+  elim (da_inv_lref … Hd1) -Hd1 * #K0 #V0 [| #d0 ] #HK0 #HV0 [| #H1 ]
+  lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
+  lapply (le_plus_to_le_c … Hd21) -Hd21 #Hd21
+  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
+  elim (lsubsv_inv_pair2 … H) -H * #K1
+  [ #HK12 #H destruct
+    elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X
+    lapply (drop_fwd_drop2 … HLK1)
+    elim (lift_total X 0 (i+1))
+    /3 width=12 by lstas_succ, cpcs_lift, ex2_intro/
+  | #V1 #d1 #H0 #_ #HV1 #HV #HK12 #_ #H destruct
+    lapply (da_mono … HV0 … HV) -HV #H destruct
+    elim (shnv_inv_cast … H0) -H0 #_ #_ #H
+    lapply (H … Hd21) -H #HVV1
+    elim (IHVW … Hd21 HV0 … HK12) -K2 -Hd21 #X #HVX #HXW
+    elim (da_lstas … HV1 (d2+1)) -HV1 #X1 #HVX1 #_
+    lapply (scpes_inv_lstas_eq … HVV1 … HVX … HVX1) -HVV1 -HVX #HXX1
+    lapply (cpcs_canc_sn … HXX1 … HXW) -X
+    elim (lift_total X1 0 (i+1))
+    lapply (drop_fwd_drop2 … HLK1)
+    /4 width=12 by cpcs_lift, lstas_cast, lstas_ldef, ex2_intro/
+  ]
+| #a #I #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
+  lapply (da_inv_bind … Hd2) -Hd2 #Hd2
+  elim (IHTU2 … Hd2 (L1.ⓑ{I}V2) …)
+  /3 width=3 by lsubsv_pair, lstas_bind, cpcs_bind_dx, ex2_intro/
+| #G #L2 #V2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
+  lapply (da_inv_flat … Hd2) -Hd2 #Hd2
+  elim (IHTU2 … Hd2 … HL12) -L2
+  /3 width=5 by lstas_appl, cpcs_flat, ex2_intro/
+| #G #L2 #W2 #T2 #U2 #d1 #_ #IHTU2 #d2 #Hd12 #Hd2 #L1 #HL12
+  lapply (da_inv_flat … Hd2) -Hd2 #Hd2
+  elim (IHTU2 … Hd2 … HL12) -L2
+  /3 width=3 by lstas_cast, ex2_intro/
+]
+qed-.
+
+lemma lsubsv_sta_trans: ∀h,o,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •*[h, 1] U2 →
+                        ∀d. ⦃G, L2⦄ ⊢ T ▪[h, o] d+1 →
+                        ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
+                        ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, 1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
+/2 width=7 by lsubsv_lstas_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsuba.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsuba.etc
new file mode 100644
index 000000000..51d490222
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsuba.etc
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/equivalence/scpes_aaa.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Forward lemmas on lenv refinement for atomic arity assignment ************)
+
+lemma lsubsv_fwd_lsuba: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃⁝ L2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_pair/
+#L1 #L2 #W #V #d1 #H #_ #_ #_ #_ #IHL12
+elim (shnv_inv_cast … H) -H #HW #HV #H
+lapply (H 0 ?) // -d1 #HWV
+elim (snv_fwd_aaa … HW) -HW #B #HW
+elim (snv_fwd_aaa … HV) -HV #A #HV
+lapply (scpes_aaa_mono … HWV … HW … HV) #H destruct
+/4 width=5 by lsuba_aaa_conf, lsuba_beta, aaa_cast/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsubd.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsubd.etc
new file mode 100644
index 000000000..7f9e72946
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_lsubd.etc
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "static_2/static/lsubd.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Forward lemmas on lenv refinement for degree assignment ******************)
+
+lemma lsubsv_fwd_lsubd: ∀h,o,G,L1,L2. G ⊢ L1 ⫃¡[h, o] L2 → G ⊢ L1 ⫃▪[h, o] L2.
+#h #o #G #L1 #L2 #H elim H -L1 -L2 /2 width=3 by lsubd_pair, lsubd_beta/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_scpds.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_scpds.etc
new file mode 100644
index 000000000..cac43d361
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_scpds.etc
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "static_2/static/lsubd_da.ma".
+include "basic_2/dynamic/lsubsv_lsubd.ma".
+include "basic_2/dynamic/lsubsv_lstas.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on decomposed extended parallel computation on terms **********)
+
+lemma lsubsv_scpds_trans: ∀h,o,G,L2,T1,T2,d. ⦃G, L2⦄ ⊢ T1 •*➡*[h, o, d] T2 →
+                          ∀L1. G ⊢ L1 ⫃¡[h, o] L2 →
+                          ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
+#h #o #G #L2 #T1 #T2 #d2 * #T #d1 #Hd21 #Hd1 #HT1 #HT2 #L1 #HL12
+lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
+elim (lsubsv_lstas_trans … HT1 … Hd1 … HL12) // #T0 #HT10 #HT0
+lapply (cpcs_cprs_strap1 … HT0 … HT2) -T #HT02
+elim (cpcs_inv_cprs … HT02) -HT02
+/5 width=5 by lsubsv_fwd_lsubd, lsubd_da_trans, ex4_2_intro, ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc
new file mode 100644
index 000000000..365849c36
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/dynamic/lsubsv_scpds.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties concerning stratified native validity *************************)
+
+lemma lsubsv_snv_trans: ∀h,o,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, o] →
+                        ∀L1. G ⊢ L1 ⫃¡[h, o] L2 → ⦃G, L1⦄ ⊢ T ¡[h, o].
+#h #o #G #L2 #T #H elim H -G -L2 -T //
+[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12
+  elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+  elim (lsubsv_inv_pair2 … H) -H * #K1
+  [ #HK12 #H destruct /3 width=5 by snv_lref/
+  | #W #d #HVW #_ #_ #_ #_ #H1 #H2 destruct -IHV
+    /3 width=6 by shnv_inv_snv, snv_lref/
+  ]
+| #a #I #G #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 destruct
+  /4 width=1 by snv_bind, lsubsv_pair/
+| #a #G #L2 #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 #IHV #IHT #L1 #HL12
+  elim (lsubsv_scpds_trans … HVW0 … HL12) -HVW0 #V0 #HV0 #HWV0
+  elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X #HT0 #H
+  elim (cprs_inv_abst1 … H) -H #W #T0 #HW0 #_ #H destruct
+  elim (cprs_conf … HWV0 … HW0) -W0
+  /4 width=10 by snv_appl, scpds_cprs_trans, cprs_bind/
+| #G #L2 #U #T #U0 #_ #_ #HU0 #HTU0 #IHU #IHT #L1 #HL12
+  elim (lsubsv_scpds_trans … HTU0 … HL12) -HTU0 #X0 #HTX0 #H1
+  elim (lsubsv_scpds_trans … HU0 … HL12) -HU0 #X #HUX #H2
+  elim (cprs_conf … H1 … H2) -U0 /3 width=5 by snv_cast, scpds_cprs_trans/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/nativevalid_6.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/nativevalid_6.etc
new file mode 100644
index 000000000..92363e0ec
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/nativevalid_6.etc
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o, break term 46 d ] )"
+   non associative with precedence 45
+   for @{ 'NativeValid $h $o $d $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/shnv.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/shnv.etc
new file mode 100644
index 000000000..961643418
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/shnv/shnv.etc
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/nativevalid_6.ma".
+include "basic_2/equivalence/scpes.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED HIGHER NATIVE VALIDITY FOR TERMS ******************************)
+
+inductive shnv (h) (o) (d1) (G) (L): predicate term ≝
+| shnv_cast: ∀U,T. ⦃G, L⦄ ⊢ U ¡[h, o] → ⦃G, L⦄ ⊢ T ¡[h, o] →
+             (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T) →
+             shnv h o d1 G L (ⓝU.T)
+.
+
+interpretation "stratified higher native validity (term)"
+   'NativeValid h o d G L T = (shnv h o d G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact shnv_inv_cast_aux: ∀h,o,G,L,X,d1. ⦃G, L⦄ ⊢ X ¡[h, o, d1] → ∀U,T. X = ⓝU.T →
+                        ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
+                         & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
+#h #o #G #L #X #d1 * -X
+#U #T #HU #HT #HUT #U1 #T1 #H destruct /3 width=1 by and3_intro/
+qed-.
+
+lemma shnv_inv_cast: ∀h,o,G,L,U,T,d1. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, d1] →
+                     ∧∧ ⦃G, L⦄ ⊢ U ¡[h, o] & ⦃G, L⦄ ⊢ T ¡[h, o]
+                      & (∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ U •*⬌*[h, o, d2, d2+1] T).
+/2 width=3 by shnv_inv_cast_aux/ qed-.
+
+lemma shnv_inv_snv: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ¡[h, o, d] → ⦃G, L⦄ ⊢ T ¡[h, o].
+#h #o #G #L #T #d * -T
+#U #T #HU #HT #HUT elim (HUT 0) -HUT /2 width=3 by snv_cast/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma snv_shnv_cast: ∀h,o,G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o] → ⦃G, L⦄ ⊢ ⓝU.T ¡[h, o, 0].
+#h #o #G #L #U #T #H elim (snv_inv_cast … H) -H
+#U0 #HU #HT #HU0 #HTU0 @shnv_cast // -HU -HT
+#d #H <(le_n_O_to_eq … H) -d /2 width=3 by scpds_div/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
index 78eeb36a2..ff9313322 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ [ break term 46 h, break term 46 o ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃![ break term 46 a, break term 46 h ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEqV $h $o $G $L1 $L2 }.
+   for @{ 'LRSubEqV $a $h $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
deleted file mode 100644
index 92363e0ec..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o, break term 46 d ] )"
-   non associative with precedence 45
-   for @{ 'NativeValid $h $o $d $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index e6a1ea5d3..1c19f4e3a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -28,16 +28,10 @@ table {
              [ [ "" ] "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
           }
         ]
-        [ { "local env. ref. for stratified native validity" * } {
-             [ [ "" ] "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
-          }
-        ]
-*)        
-        [ { "context-sensitive native validity" * } {
-(*
-             [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
 *)
-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ]
+        [ { "context-sensitive native validity" * } {
+             [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "snv_cpm_trans" (* + "snv_scpes" + "snv_preserve" *) * ]
           }
         ]
      }
@@ -127,6 +121,7 @@ class "capitalize italic" { 0 1 }
 
 class "italic"            { 2 }
 (*
+             [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
         [ { "decomposed rt-equivalence" * } {
              [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
           }