From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 18 Jun 2014 15:03:20 +0000 (+0000)
Subject: milestone connit for preservation:
X-Git-Tag: make_still_working~899
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcab3f92c6f815098ecc24eff06bfd3d232eb497;p=helm.git

milestone connit for preservation:
- for now we remove stratified equivalence for terms
  (it is much more complicated than expected)
- we park in etc a generalization of preservation
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_cpcs.etc
new file mode 100644
index 000000000..9e68edfce
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_cpcs.etc
@@ -0,0 +1,182 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unfold/lstas_lstas.ma".
+include "basic_2/computation/fpbs_lift.ma".
+include "basic_2/computation/fpbg_fleq.ma".
+include "basic_2/equivalence/cpes_cpds.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_snv_cpx_lpx: ∀h:sh. sd h → relation3 genv lenv term ≝
+                           λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                           ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+
+definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+                          λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                          ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+                          ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                          ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+
+definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝
+                             λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                             ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+                             ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+                             ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                             ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+
+(* Properties for the preservation results **********************************)
+
+fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                      ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+/3 width=6 by lpr_lpx, cpr_cpx/ qed-.
+
+fact snv_sta_aux: ∀h,g,G0,L0,T0.
+                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                  ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] →
+                  ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
+                  ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g].
+/3 width=6 by sta_cpx/ qed-.
+
+fact snv_cpxs_lpx_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
+@(cpxs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cpxs_fpbs/
+qed-.
+
+fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g].
+/3 width=10 by snv_cpxs_lpx_aux, cprs_cpxs, lpr_lpx/ qed-.
+
+fact snv_lstas_aux: ∀h,g,G0,L0,T0.
+                    (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                    ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                    ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+                    ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → ⦃G, L1⦄ ⊢ U1 ¡[h, g].
+/3 width=12 by snv_cpxs_lpx_aux, lstas_cpxs/ qed-.
+
+fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                      ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                      ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H
+@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/
+qed-.
+
+fact da_cpcs_aux: ∀h,g,G0,L0,T0.
+                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                  (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                  ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+                  ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
+                  ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
+                  ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H
+elim (cpcs_inv_cprs … H) -H /4 width=18 by da_cprs_lpr_aux, da_mono/
+qed-.
+
+fact sta_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                      ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                      ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 →
+                      ∀U1. ⦃G, L1⦄ ⊢ T1 •[h] U1 →
+                      ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                      ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #H01 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12
+elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) -H01 -Hl -HT12 -HL12
+/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/
+qed-.
+
+fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0.
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                         ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                         ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+                         ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+                         ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                         ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2
+[2: /3 width=12 by da_cprs_lpr_aux/
+|3: /3 width=10 by snv_cprs_lpr_aux/
+|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/
+] -G0 -L0 -T0 -T1 -T -l1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+fact lstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0.
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                         (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                         ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                         ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
+                         ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+                         ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
+                         ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (lstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1
+elim (lstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0
+lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
+qed-.
+
+fact lstas_cpds_aux: ∀h,g,G0,L0,T0.
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                     ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
+                     ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 →
+                     ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 →
+                     ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2
+lapply (da_mono … H … Hl1) -H #H destruct
+lapply (lstas_da_conf … HTU1 … Hl1) #Hl12
+elim (le_or_ge l2 l) #Hl2
+[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T
+  /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/
+| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l
+  lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1
+  elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) -IH2 -IH1 -Hl1l -HTU1 -HTT2
+  /3 width=12 by snv_lstas_aux, cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l, ex3_2_intro/
+]
+qed-.
+
+fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                       (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                       ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+                       ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 →
+                       ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+                       ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12
+lapply (IH2 … H01 … Hl1 … HT12 … HL12) -L0 -T0 // -T1
+lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_da_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_da_lpr.etc
new file mode 100644
index 000000000..119a40243
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_da_lpr.etc
@@ -0,0 +1,93 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/static/lsubd_da.ma".
+include "basic_2/computation/cpds_cpds.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on degree assignment for terms ********************************)
+
+fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                     (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                     ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h g G1 L1 T1.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH2 -IH1
+  lapply (da_inv_sort … H2) -H2
+  lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1 by da_sort/
+| #i #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH2
+  elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #H #HX0
+  elim (da_inv_lref … H2) -H2 * #K1 [ #V1 | #W1 #l1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct
+  lapply (ldrop_mono … H … HLK1) -H #H destruct
+  elim (cpr_inv_lref1 … H3) -H3
+  [1,3: #H destruct
+    lapply (fqup_lref … G1 … HLK1)
+    elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
+    elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+    /4 width=10 by da_ldef, da_ldec, fqup_fpbg/
+  |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0
+    lapply (ldrop_mono … H … HLK1) -H #H destruct
+    lapply (fqup_lref … G1 … HLK1)
+    elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
+    elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
+    lapply (ldrop_fwd_drop2 … HLK2) -V2
+    /4 width=8 by da_lift, fqup_fpbg/
+  ]
+| #p #_ #_ #HT0 #H1 destruct -IH2 -IH1
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH2
+  elim (snv_inv_bind … H1) -H1 #_ #HT1
+  lapply (da_inv_bind … H2) -H2
+  elim (cpr_inv_bind1 … H3) -H3 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
+  | #T2 #HT12 #HT2 #H1 #H2 destruct
+    /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_drop/
+  ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct
+  elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10
+  lapply (da_inv_flat … H2) -H2 #Hl
+  elim (cpr_inv_appl1 … H3) -H3 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct -IH2 /4 width=7 by da_flat, fqup_fpbg/
+  | #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW #HU1
+    lapply (da_inv_bind … Hl) -Hl #Hl
+    elim (cpds_inv_abst1 … HT10) -HT10 #W3 #U3 #HW3 #_ #H destruct -U3
+    lapply (cprs_div … HW3 … HW10) -W3 #HWW1
+    lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #H
+    elim (snv_fwd_da … HW) #l1 #Hl1
+    lapply (snv_lstas_aux … IH2 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbg, sta_lstas/ #HW1
+    lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_fpbs/ #H destruct
+    lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbg/ ] #Hl0
+    lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbg/ -HW
+    lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
+    /4 width=6 by da_bind, lsubd_da_trans, lsubd_abbr/
+  | #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH2 -V -W0 -T0 -l0 -HV1 -HVW1
+    elim (snv_inv_bind … HT1) -HT1 #_
+    lapply (da_inv_bind … Hl) -Hl
+    /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/
+  ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH2
+  elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1
+  lapply (da_inv_flat … H2) -H2 #Hl
+  elim (cpr_inv_cast1 … H3) -H3
+  [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/
+  | /3 width=7 by fqup_fpbg/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lpx.etc
new file mode 100644
index 000000000..0839b45b2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lpx.etc
@@ -0,0 +1,135 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/snv_lift.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/lsubsv_snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+fact snv_cpx_lpx_aux: ∀h,g,G0,L0,T0.
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                      (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                      ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpx_lpx h g G1 L1 T1.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH3 -IH2 -IH1 -H1
+  elim (cpx_inv_sort1 … H2) -H2 // * //
+| #i #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH3 -IH2
+  elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
+  elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (fqup_lref … G1 … HLK1) #HKL
+  elim (cpx_inv_lref1 … H2) -H2
+  [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
+  | * #I0 #K0 #V0 #W0 #H #HVW0 #W0 -HV12
+    lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
+    lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=8 by fqup_fpbg, snv_lift/
+  ]
+| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH3 -IH2 -IH1
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH3 -IH2
+  elim (snv_inv_bind … H1) -H1 #HV1 #HT1
+  elim (cpx_inv_bind1 … H2) -H2 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpx_pair/
+  | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
+    /4 width=10 by fqup_fpbg, snv_inv_lift, lpx_pair, ldrop_drop/
+  ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
+  elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1
+  elim (cpx_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
+(*    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0
+    elim (sta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12
+    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H
+    elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct
+    lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10
+    lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
+    lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
+    elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
+    lapply (cpds_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?)
+    /2 width=7 by snv_appl, cprs_bind/ *)
+  | #b #V2 #W20 #W2 #T20 #T2 #HV12 #HW202 #HT202 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
+    elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
+    lapply (cprs_div … HW10 … HW230) -W30 #HW120
+    lapply (snv_sta_aux … IH1 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10
+    lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #HlW10
+    elim (snv_fwd_da … HW20) #l #Hl
+    lapply (da_cpcs_aux … IH1 IH2 … HlW10 … Hl … HW120) // -HlW10
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_fpbs/ #H destruct
+(*    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HlV2
+    lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fqup_fpbg/ #HlW2
+    elim (sta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #W3 #HV2W3 #HW103
+    lapply (da_sta_conf … HV2W3 … HlV2) <minus_plus_m_m #HlW3
+    lapply (cpcs_cpr_strap1 … HW120 … HW202) -HW120 #HW102
+    lapply (lpr_cpcs_conf … HL12 … HW102) -HW102 #HW102
+    lapply (cpcs_canc_sn … HW103 … HW102) -W10 #HW32
+    lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 #HV2
+    lapply (IH1 … HW202 … HL12) /2 width=1 by fqup_fpbg/ -HW20 #HW2
+    lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT20 #HT2
+    lapply (snv_sta_aux … IH4 … HlV2 … HV2W3)
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW3
+    lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
+    @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
+    lapply (lstas_sta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
+    @(lstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
+    [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/
+    | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
+    ] *)
+  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
+    elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+    elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
+(*    lapply (lpr_cpr_conf … HL12 … HW10) -HW10 #HW10 
+    elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H
+    elim (cprs_inv_abst1 … H) -H #W #U2 #HW1 #_ #H destruct -U3
+    elim (sta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2
+    lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
+    elim (lift_total X 0 1) #W20 #H3
+    lapply (sta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=2 by ldrop_drop/ -H1 #HVW20
+    lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=2 by ldrop_drop/ -HW13 -H3 -H2 #HW320
+    lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
+    elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
+    lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
+    lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
+    lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=2 by ldrop_drop/ -Hl0 #Hl0
+    lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
+    lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
+    lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
+    lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_drop/ *)
+  ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
+  elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1
+  elim (cpx_inv_cast1 … H2) -H2
+  [ * #W2 #T2 #HW12 #HT12 #H destruct
+(*    lapply (cpcs_cprs_strap1 … HUW1 W2 ?) /2 width=1 by cpr_cprs/ -HUW1 #H1
+*)    lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ -HW1 -HW12 #HW2
+    lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH1 #HT2
+(*    elim (sta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HTU1 #U2 #HTU2 #HU12
+    lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -HT1 -HT12 -Hl0 #Hl0
+    /4 width=7 by snv_cast, lpr_cpcs_conf, cpcs_canc_sn/ *)
+  | #H -IH3 -IH2 -HW1 -HTU1 -HUW1
+    lapply (IH1 … H … HL12) -IH1 -H -HL12 /2 width=1 by fqup_fpbg/
+  | #H -IH3 -IH2 -HTU1 -HUW1
+    lapply (IH1 … H … HL12) -IH1 -H -HL12 /2 width=1 by fqup_fpbg/
+  ]
+]
+[4: @snv_cast //
+qed-.
+snv_lstas, snv_cpr_lpr
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas_lpr.etc
new file mode 100644
index 000000000..3e1ed02d6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv/snv_lstas_lpr.etc
@@ -0,0 +1,150 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/computation/cpds_cpds.ma".
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/lsubsv_lstas.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on sn parallel reduction for local environments ***************)
+
+fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                        (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
+                        ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_cpr_lpr h g G1 L1 T1.
+#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+[ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1
+  >(lstas_inv_sort1 … H2) -X2
+  >(cpr_inv_sort1 … H3) -X3 /2 width=3 by ex2_intro/
+| #i #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH3
+  [ lapply (lstas_inv_O … H2) -H2 #H destruct -IH1 -H1 -l1 /4 width=5 by lpr_cpcs_conf, cpr_cpcs_dx, ex2_intro/ ]
+  elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HK0 #HX0
+  elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l0 ] #HLK1 [ #HVl1 | #HWl1 #H destruct ]
+  lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct
+  elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #W0 [2,4: #X0 ] #HK0 [1,2: #_ -X0 ] #HVW0 #HX2
+  lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct
+  [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ]
+  lapply (fqup_lref … G1 … HLK1) #HKV1
+  elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct
+  lapply (ldrop_fwd_drop2 … HLK2) #H2
+  elim (cpr_inv_lref1 … H3) -H3
+  [1,3: #H destruct -HLK1
+  |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0
+        lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct
+  ]
+  [ lapply (IH2 … HWl1 … HW12 … HK12) /2 width=1 by fqup_fpbg/ -IH2 #H
+    elim (da_inv_sta … H) -H
+    elim (IH1 … HWl1 … HVW0 … HW12 … HK12) -IH1 -HVW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
+    elim (lift_total V2 0 (i+1))
+    /3 width=12 by cpcs_lift, lstas_ldec, ex2_intro/
+  | elim (IH1 … HVl1 … HVW0 … HV12 … HK12) -IH1 -HVl1 -HVW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
+    elim (lift_total W2 0 (i+1))
+    /4 width=12 by cpcs_lift, lstas_ldef, ex2_intro/
+  | elim (IH1 … HVl1 … HVW0 … HVX0 … HK12) -IH1 -HVl1 -HVW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02
+    elim (lift_total W2 0 (i+1))
+    /3 width=12 by cpcs_lift, lstas_lift, ex2_intro/
+  ]
+| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
+  elim (snv_inv_gref … H1)
+| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+  elim (snv_inv_bind … H1) -H1 #_ #HT1
+  lapply (da_inv_bind … Hl1) -Hl1 #Hl1
+  elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct
+  elim (cpr_inv_bind1 … H3) -H3 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1
+    /4 width=5 by cpcs_bind2, lpr_cpr_conf, lstas_bind, ex2_intro/
+  | #T3 #HT13 #HXT3 #H1 #H2 destruct
+    elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
+    elim (lstas_inv_lift1 … HTU3 L2 … HXT3) -T3
+    /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_drop, ex2_intro/
+  ]
+| #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct
+  elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10
+  lapply (da_inv_flat … Hl1) -Hl1 #Hl1
+  elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct
+  elim (cpr_inv_appl1 … H3) -H3 *
+  [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2
+    elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1
+    /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lstas_appl, ex2_intro/
+  | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct
+    elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2
+    lapply (da_inv_bind … Hl1) -Hl1 #Hl1
+    elim (lstas_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
+    elim (cpds_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW20 #_ #H destruct
+    lapply (cprs_div … HW10 … HW20) -W0 #HW12
+    lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #H
+    elim (snv_fwd_da … HW2) #l #Hl
+    lapply (snv_lstas_aux … IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbg, sta_lstas/ #HW1
+    lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
+    /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_fpbs/ #H destruct
+    lapply (snv_cpr_lpr_aux … IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+    lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2l
+    elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fqup_fpbg, sta_lstas/ -HVW1 #W4 #H #HW14
+    lapply (lstas_inv_SO … H) #HV2W4
+    lapply (da_sta_conf … HV2W4 … HV2l) <minus_plus_m_m #HW4l
+    lapply (snv_lstas_aux … IH3 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW4
+    lapply (snv_cpr_lpr_aux … IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
+    lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3l
+    elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23
+    lapply (cpcs_cpr_strap1 … HW12 … HW23) #H
+    lapply (lpr_cpcs_conf … HL12 … H) -H #H
+    lapply (cpcs_canc_sn … HW14 H) -H #HW43
+    elim (lsubsv_lstas_trans … g … HTU3 … Hl21 … (L2.ⓓⓝW3.V2)) -HTU3
+    [ #U4 #HT3U4 #HU43 -HW12 -HW3 -HW3l -W4 -IH3 -IH2
+      @(ex2_intro … (ⓓ{b}ⓝW3.V2.U4)) /2 width=1 by lstas_bind/ -HT3U4
+      @(cpcs_canc_dx … (ⓓ{b}ⓝW3.V2.U3)) /2 width=1 by cpcs_bind_dx/ -HU43
+      @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/
+      /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
+    | -U3
+      @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/
+      #W #W0 #l0 #Hl0 #HV2W #HW30
+      lapply (lstas_sta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W
+      @(lstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) //
+      [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/
+      | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/
+      ]
+    | -IH3 -IH1 /3 width=9 by fqup_fpbg, lpr_pair/
+    ]
+  | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH3 -IH2
+    elim (snv_inv_bind … HT1) -HT1 #_ #HT0
+    lapply (da_inv_bind … Hl1) -Hl1 #Hl1
+    elim (lstas_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct
+    elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02
+    lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10
+    lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02
+    lapply (cpcs_bind2 b … HW02 … HU02) -HW02 -HU02 #HU02
+    lapply (cpcs_flat … HV10 … HU02 Appl) -HV10 -HU02 #HU02
+    lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?)
+    /4 width=3 by lstas_appl, lstas_bind, cpr_theta, ex2_intro/
+  ]
+| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
+  [ lapply (lstas_inv_O … H2) -H2 #H destruct -IH1 -H1 -l1 /4 width=5 by lpr_cpcs_conf, cpr_cpcs_dx, ex2_intro/ ]
+  elim (snv_inv_cast … H1) -H1 #U1 #l #_ #HT1 #_ #_ #_ -U1 -l
+  lapply (da_inv_flat … Hl1) -Hl1 #Hl1
+  lapply (lstas_inv_cast1 … H2) -H2 #HTU1
+  elim (cpr_inv_cast1 … H3) -H3
+  [ * #U2 #T2 #_ #HT12 #H destruct
+    elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 -HL12
+    /3 width=3 by fqup_fpbg, lstas_cast, ex2_intro/
+  | #HT1X3
+    elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12
+    /2 width=3 by fqup_fpbg, ex2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/extra.txt b/matita/matita/contribs/lambdadelta/basic_2/extra.txt
new file mode 100644
index 000000000..6a9a493e7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/extra.txt
@@ -0,0 +1,7 @@
+basic_2/static/lsuba_lsuba.ma
+basic_2/static/sta_llpx_sn.ma
+basic_2/computation/fpbu_lift.ma
+basic_2/computation/fpbg_lift.ma
+basic_2/computation/lpxs_aaa.ma
+basic_2/computation/lsubc_lsuba.ma
+basic_2/dynamic/lsubsv_lsuba.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/steq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/steq.ma
deleted file mode 100644
index 9c8906286..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/static/steq.ma
+++ /dev/null
@@ -1,41 +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/lazyeq_4.ma".
-include "basic_2/grammar/term.ma".
-include "basic_2/static/sd.ma".
-
-(* STRATIFIED EQUIVALENCE FOR TERMS *****************************************)
-
-inductive steq (h) (g): relation term ≝
-| steq_refl: ∀T. steq h g T T
-| steq_zero: ∀k1,k2. deg h g k1 0 → deg h g k2 0 → steq h g (⋆k1) (⋆k2)
-.
-
-interpretation
-   "stratified equivalence (term)"
-   'LazyEq h g T1 T2 = (steq h g T1 T2).
-
-(* Basic inversion lemmas ****************************************************)
-
-lemma steq_inv: ∀h,g,T1,T2. T1 ≡[h, g] T2 → T1 = T2 ∨
-                ∃∃k1,k2. deg h g k1 0 & deg h g k2 0 & T1 = ⋆k1 & T2 = ⋆k2.
-#h #g #T1 #T2 * /3 width=6 by or_introl, or_intror, ex4_2_intro/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma steq_sym: ∀h,g. symmetric … (steq h g).
-#h #g #T1 #T2 * /2 width=1 by steq_zero/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/steq_steq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/steq_steq.ma
deleted file mode 100644
index 4cf9b752c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/static/steq_steq.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/static/steq.ma".
-
-(* STRATIFIED EQUIVALENCE FOR TERMS *****************************************)
-
-(* Main properties **********************************************************)
-
-theorem steq_trans: ∀h,g. Transitive … (steq h g).
-#h #g #T1 #T * //
-#k1 #k #Hk1 #HK2 #X #H elim (steq_inv … H) -H /2 width=1 by steq_zero/
-* /2 width=1 by steq_zero/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index 4ccbf25fc..7a26896f5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -31,9 +31,9 @@
          Context-sensitive subject equivalence
          for native type assignment.
    </news>
-   <news date="In progress.">
+   <news date="2014 June 18.">
          Preservation of stratified native validity
-         for "big tree" computation on closures.
+         for context-sensitive computation on terms.
    </news>
    <news date="2014 June 9.">
          "Big tree" strong normalization
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 1c4072923..5a106401c 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
@@ -185,10 +185,6 @@ table {
              [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_sta" + "da_da" * ]
           }
         ]
-        [ { "stratified equivalence" * } {
-             [ "steq ( ? ≡[?,?] ? )" "steq_steq" * ]
-          }
-        ]
         [ { "static type assignment" * } {
              [ "sta ( ⦃?,?⦄ ⊢ ? •[?] ? )" "sta_lift" + "sta_lpx_sn" + "sta_aaa" + "sta_sta" * ]
           }
diff --git a/matita/matita/contribs/lambdadelta/extra.txt b/matita/matita/contribs/lambdadelta/extra.txt
deleted file mode 100644
index 6a9a493e7..000000000
--- a/matita/matita/contribs/lambdadelta/extra.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-basic_2/static/lsuba_lsuba.ma
-basic_2/static/sta_llpx_sn.ma
-basic_2/computation/fpbu_lift.ma
-basic_2/computation/fpbg_lift.ma
-basic_2/computation/lpxs_aaa.ma
-basic_2/computation/lsubc_lsuba.ma
-basic_2/dynamic/lsubsv_lsuba.ma