From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 14 Mar 2013 23:06:19 +0000 (+0000)
Subject: - main proof case closed in the 4th component of preservation
X-Git-Tag: make_still_working~1217
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=132d053caaeb9f8311fb0c807a9d7fd8d7acc827;hp=603c8b3cdab901c26f63b5fed2c65e49693cc9a3;p=helm.git

- main proof case closed in the 4th component of preservation
- bug fix in Makefile: now both xoa and probe receive both
configuration files
- useless notion lsubss removed (to be replaced by lsubse)
---

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 3e5b74eaf..8493b47c0 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -3,11 +3,13 @@ H    := @
 
 TRIM := sed "s/ \\+$$//"
 
-XOA_DIR     := ../../../components/binaries/xoa
-XOA         := xoa.native
 XOA_CONF    := ground_2/xoa.conf.xml
 XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma
 
+XOA_DIR     := ../../../components/binaries/xoa
+XOA         := xoa.native
+XOA_OPTS    := ../../matita.conf.xml $(XOA_CONF)
+
 DEP_DIR     := ../../../components/binaries/matitadep
 DEP         := matitadep.native
 
@@ -16,7 +18,7 @@ MAC         := mac.native
 
 PRB_DIR     := ../../../components/binaries/probe
 PRB         := probe.native
-PRB_OPTS    := ../../matita.conf.xml $(XOA_CONF) -g 
+PRB_OPTS    := $(XOA_OPTS) -g 
 
 ORIG        := . ./orig.sh 
 ORIGS       := basic_2/basic_1.orig
@@ -50,7 +52,7 @@ xoa: $(XOA_TARGETS)
 
 $(XOA_TARGETS): $(XOA_CONF)
 	@echo "  EXEC $(XOA) $(XOA_CONF)"
-	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_CONF)
+	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_OPTS)
 
 # orig #######################################################################
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma
deleted file mode 100644
index b1e340b2c..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lsubss.ma
+++ /dev/null
@@ -1,26 +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/unwind/sstas_lsubss.ma".
-include "basic_2/computation/dxprs.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-(* Properties on lenv ref for stratified type assignment ********************)
-
-lemma lsubss_dxprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
-                          ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2.
-#h #g #L1 #L2 #HL12 #T1 #T2 *
-lapply (lsubss_fwd_lsubs2 … HL12) /3 width=5/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
index f3238fbd9..2afaa8e06 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma
@@ -66,15 +66,14 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
   | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
     elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
     elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
-    lapply (cprs_div … HW230 … HW10) -W30 #HW210
-    lapply (ltpr_cpcs_conf … HL12 … HW210) -HW210 #HW210
+    lapply (cprs_div … HW10 … HW230) -W30 #HW120
+    elim (snv_fwd_ssta … HW20) #U20 #l0 #HWU20
+    elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #U10 #HWU10
+    elim (ssta_ltpr_cpcs_aux … IH1 IH3 … HW20 … HWU10 … HWU20) // -IH3 -HWU10
+    [2: /3 width=5/ |3: /2 width=1/
+    |4: /4 width=4 by ygt_yprs_trans, ypr_yprs, ypr_ssta, fw_ygt/
+    ] #H #_ -IH2 -U10 destruct
+    lapply (IH4 … HT20 (L1.ⓓV1) ?) [ /2 width=6/ | /2 width=1/ ] -U20 -W10 -l0 -IH4 -HT20 -HW20 #HT20
     lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
-    lapply (IH1 … HW20 … HL12 W20 ?) // [ /2 width=1/ ] -HW20 #HW20
-    lapply (IH1 … HT20 … (L2.ⓛW20) … HT202) [1,2: /2 width=1/ ] -IH1 -HT20 -HT202 #HT2
-    elim (IH3 … HVW1 … HL12 … HV12) // [2: /2 width=1/ ] -HV1 -HVW1 -HV12 #W200 #HVW200 #H
-    lapply (cpcs_trans … HW210 … H) -W10 #HW200
-    lapply (IH4 … HT2 (L2.ⓓV2) ?) -HT2
-    [ (* /2 width=4/ *)
-    |
-    | /2 width=1/
-    ] 
+    lapply (IH1 … HT20 … (L2.ⓓV2) … HT202) [1,2: /2 width=1/ ] -L1 -V1 -W20 -T20 /2 width=1/
+  |
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/dxprs_lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/dxprs_lsubss.etc
new file mode 100644
index 000000000..b1e340b2c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/dxprs_lsubss.etc
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind/sstas_lsubss.ma".
+include "basic_2/computation/dxprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_dxprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                          ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2.
+#h #g #L1 #L2 #HL12 #T1 #T2 *
+lapply (lsubss_fwd_lsubs2 … HL12) /3 width=5/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss.etc
new file mode 100644
index 000000000..7e9751a9f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss.etc
@@ -0,0 +1,105 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ssta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+inductive lsubss (h:sh) (g:sd h): relation lenv ≝
+| lsubss_atom: lsubss h g (⋆) (⋆)
+| lsubss_pair: ∀I,L1,L2,W. lsubss h g L1 L2 →
+               lsubss h g (L1. ⓑ{I} W) (L2. ⓑ{I} W)
+| lsubss_abbr: ∀L1,L2,V,W,l. ⦃h, L1⦄ ⊢ V •[g, l+1] W → ⦃h, L2⦄ ⊢ V •[g, l+1] W →
+               lsubss h g L1 L2 → lsubss h g (L1. ⓓV) (L2. ⓛW)
+.
+
+interpretation
+  "local environment refinement (stratified static type assigment)"
+  'CrSubEqS h g L1 L2 = (lsubss h g L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
+#h #g #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆.
+/2 width=5/ qed-.
+
+fact lsubss_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                           ∀I,K1,V. L1 = K1. ⓑ{I} V →
+                           (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
+                           ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+                                     h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
+#h #g #L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubss_inv_pair1: ∀h,g,I,K1,L2,V. h ⊢ K1. ⓑ{I} V •⊑[g] L2 →
+                        (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
+                        ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+                                  h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
+/2 width=3/ qed-.
+
+fact lsubss_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
+#h #g #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
+]
+qed.
+
+lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆.
+/2 width=5/ qed-.
+
+fact lsubss_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                           ∀I,K2,W. L2 = K2. ⓑ{I} W →
+                           (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
+                           ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+                                     h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
+#h #g #L1 #L2 * -L1 -L2
+[ #I #K2 #W #H destruct
+| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
+| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 •⊑[g] K2. ⓑ{I} W →
+                        (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
+                        ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
+                                  h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
+/2 width=3/ qed-.
+
+(* Basic_forward lemmas *****************************************************)
+
+lemma lsubss_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubss_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L.
+#h #g #L elim L -L // /2 width=1/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ldrop.etc
new file mode 100644
index 000000000..82ede6149
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ldrop.etc
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubss.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                            ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+                            ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK1
+  [ destruct
+    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK1) -L1 /3 width=3/
+  ]
+| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK1
+  [ destruct
+    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK1) -L1 /3 width=3/
+  ]
+]
+qed.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                             ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+                             ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK2
+  [ destruct
+    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK2) -L2 /3 width=3/
+  ]
+| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #HLK2
+  [ destruct
+    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
+    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
+  | elim (IHL12 … HLK2) -L2 /3 width=3/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_lsubss.etc
new file mode 100644
index 000000000..d9f9496ba
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_lsubss.etc
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubss_ssta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STATIC TYPE ASSIGNMENT ******************)
+
+(* Main properties **********************************************************)
+
+theorem lsubss_trans: ∀h,g,L1,L. h ⊢ L1 •⊑[g] L → ∀L2. h ⊢ L •⊑[g] L2 →
+                      h ⊢ L1 •⊑[g] L2.
+#h #g #L1 #L #H elim H -L1 -L
+[ #X #H >(lsubss_inv_atom1 … H) -H //
+| #I #L1 #L #W #HL1 #IHL1 #X #H
+  elim (lsubss_inv_pair1 … H) -H * #L2
+  [ #HL2 #H destruct /3 width=1/
+  | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/
+  ]
+| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H
+  elim (lsubss_inv_pair1 … H) -H * #L2
+  [ #HL2 #H destruct /3 width=5/
+  | #V #l0 #_ #_ #_ #_ #H destruct
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc
new file mode 100644
index 000000000..f9c628921
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ssta_lift.ma".
+include "basic_2/static/ssta_ssta.ma".
+include "basic_2/static/lsubss_ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Properties concerning stratified native type assignment ******************)
+
+lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U →
+                         ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U.
+#h #g #L2 #T #U #l #H elim H -L2 -T -U -l
+[ /2 width=1/
+| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12
+  elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+  elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ]
+  [ #HK12 #H destruct /3 width=6/
+  | #V1 #l0 #_ #_ #_ #_ #H destruct
+  ]
+| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12
+  elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+  elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ]
+  [ #HK12 #H destruct /3 width=6/
+  | #V1 #l0 #H1 #H2 #_ #H #_ destruct
+    elim (ssta_fwd_correct … H2) -H2 #V #H
+    elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/
+  ]
+| /4 width=1/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U →
+                        ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U.
+#h #g #L1 #T #U #l #H elim H -L1 -T -U -l
+[ /2 width=1/
+| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12
+  elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
+  elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ]
+  [ #HK12 #H destruct /3 width=6/
+  | #V2 #l0 #H1 #H2 #_ #H #_ destruct
+    elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct
+    elim (ssta_fwd_correct … H2) -H2 /2 width=6/
+  ]
+| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12
+  elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
+  elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ]
+  [ #HK12 #H destruct /3 width=6/
+  | #V2 #l0 #_ #_ #_ #_ #H destruct
+  ]
+| /4 width=1/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc
new file mode 100644
index 000000000..5ec33634f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubss_ssta.ma".
+include "basic_2/unwind/sstas.ma".
+
+(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_sstas_trans: ∀h,g,L2,T,U. ⦃h, L2⦄ ⊢ T •*[g] U →
+                          ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •*[g] U.
+#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
+qed.
+
+lemma lsubss_sstas_conf: ∀h,g,L1,T,U. ⦃h, L1⦄ ⊢ T •*[g] U →
+                         ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •*[g] U.
+#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma
deleted file mode 100644
index 356d7fe11..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss.ma
+++ /dev/null
@@ -1,106 +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/ssta.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
-
-(* Note: may not be transitive *)
-inductive lsubss (h:sh) (g:sd h): relation lenv ≝
-| lsubss_atom: lsubss h g (⋆) (⋆)
-| lsubss_pair: ∀I,L1,L2,W. lsubss h g L1 L2 →
-               lsubss h g (L1. ⓑ{I} W) (L2. ⓑ{I} W)
-| lsubss_abbr: ∀L1,L2,V,W,l. ⦃h, L1⦄ ⊢ V •[g, l+1] W → ⦃h, L2⦄ ⊢ V •[g, l+1] W →
-               lsubss h g L1 L2 → lsubss h g (L1. ⓓV) (L2. ⓛW)
-.
-
-interpretation
-  "local environment refinement (stratified static type assigment)"
-  'CrSubEqS h g L1 L2 = (lsubss h g L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
-]
-qed.
-
-lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆.
-/2 width=5/ qed-.
-
-fact lsubss_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
-                           ∀I,K1,V. L1 = K1. ⓑ{I} V →
-                           (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
-                           ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
-                                     h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
-#h #g #L1 #L2 * -L1 -L2
-[ #I #K1 #V #H destruct
-| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
-| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/
-]
-qed.
-
-lemma lsubss_inv_pair1: ∀h,g,I,K1,L2,V. h ⊢ K1. ⓑ{I} V •⊑[g] L2 →
-                        (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
-                        ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
-                                  h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
-/2 width=3/ qed-.
-
-fact lsubss_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
-]
-qed.
-
-lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆.
-/2 width=5/ qed-.
-
-fact lsubss_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
-                           ∀I,K2,W. L2 = K2. ⓑ{I} W →
-                           (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
-                           ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
-                                     h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
-#h #g #L1 #L2 * -L1 -L2
-[ #I #K2 #W #H destruct
-| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
-| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/
-]
-qed.
-
-lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 •⊑[g] K2. ⓑ{I} W →
-                        (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
-                        ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
-                                  h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
-/2 width=3/ qed-.
-
-(* Basic_forward lemmas *****************************************************)
-
-lemma lsubss_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L1|] L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
-qed-.
-
-lemma lsubss_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 ≼[0, |L2|] L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L.
-#h #g #L elim L -L // /2 width=1/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma
deleted file mode 100644
index 82ede6149..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ldrop.ma
+++ /dev/null
@@ -1,65 +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/lsubss.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
-
-(* Properties concerning basic local environment slicing ********************)
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
-                            ∀K1,e. ⇩[0, e] L1 ≡ K1 →
-                            ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK1
-  [ destruct
-    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK1) -L1 /3 width=3/
-  ]
-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K1 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK1
-  [ destruct
-    elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK1) -L1 /3 width=3/
-  ]
-]
-qed.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
-                             ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                             ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK2
-  [ destruct
-    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK2) -L2 /3 width=3/
-  ]
-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #IHL12 #K2 #e #H
-  elim (ldrop_inv_O1 … H) -H * #He #HLK2
-  [ destruct
-    elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
-    <(ldrop_inv_refl … H) in HL12; -H /3 width=3/
-  | elim (IHL12 … HLK2) -L2 /3 width=3/
-  ]
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma
deleted file mode 100644
index d9f9496ba..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_lsubss.ma
+++ /dev/null
@@ -1,36 +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/lsubss_ssta.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STATIC TYPE ASSIGNMENT ******************)
-
-(* Main properties **********************************************************)
-
-theorem lsubss_trans: ∀h,g,L1,L. h ⊢ L1 •⊑[g] L → ∀L2. h ⊢ L •⊑[g] L2 →
-                      h ⊢ L1 •⊑[g] L2.
-#h #g #L1 #L #H elim H -L1 -L
-[ #X #H >(lsubss_inv_atom1 … H) -H //
-| #I #L1 #L #W #HL1 #IHL1 #X #H
-  elim (lsubss_inv_pair1 … H) -H * #L2
-  [ #HL2 #H destruct /3 width=1/
-  | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/
-  ]
-| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H
-  elim (lsubss_inv_pair1 … H) -H * #L2
-  [ #HL2 #H destruct /3 width=5/
-  | #V #l0 #_ #_ #_ #_ #H destruct
-  ]
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma
deleted file mode 100644
index f9c628921..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubss_ssta.ma
+++ /dev/null
@@ -1,69 +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/ssta_lift.ma".
-include "basic_2/static/ssta_ssta.ma".
-include "basic_2/static/lsubss_ldrop.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
-
-(* Properties concerning stratified native type assignment ******************)
-
-lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U →
-                         ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U.
-#h #g #L2 #T #U #l #H elim H -L2 -T -U -l
-[ /2 width=1/
-| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12
-  elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
-  elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ]
-  [ #HK12 #H destruct /3 width=6/
-  | #V1 #l0 #_ #_ #_ #_ #H destruct
-  ]
-| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12
-  elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
-  elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ]
-  [ #HK12 #H destruct /3 width=6/
-  | #V1 #l0 #H1 #H2 #_ #H #_ destruct
-    elim (ssta_fwd_correct … H2) -H2 #V #H
-    elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/
-  ]
-| /4 width=1/
-| /3 width=1/
-| /3 width=1/
-]
-qed.
-
-lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U →
-                        ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U.
-#h #g #L1 #T #U #l #H elim H -L1 -T -U -l
-[ /2 width=1/
-| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12
-  elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
-  elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ]
-  [ #HK12 #H destruct /3 width=6/
-  | #V2 #l0 #H1 #H2 #_ #H #_ destruct
-    elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct
-    elim (ssta_fwd_correct … H2) -H2 /2 width=6/
-  ]
-| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12
-  elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
-  elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ]
-  [ #HK12 #H destruct /3 width=6/
-  | #V2 #l0 #_ #_ #_ #_ #H destruct
-  ]
-| /4 width=1/
-| /3 width=1/
-| /3 width=1/
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma
deleted file mode 100644
index 5ec33634f..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lsubss.ma
+++ /dev/null
@@ -1,30 +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/lsubss_ssta.ma".
-include "basic_2/unwind/sstas.ma".
-
-(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
-
-(* Properties on lenv ref for stratified type assignment ********************)
-
-lemma lsubss_sstas_trans: ∀h,g,L2,T,U. ⦃h, L2⦄ ⊢ T •*[g] U →
-                          ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •*[g] U.
-#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
-qed.
-
-lemma lsubss_sstas_conf: ∀h,g,L1,T,U. ⦃h, L1⦄ ⊢ T •*[g] U →
-                         ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •*[g] U.
-#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
-qed.
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 ea981eaa5..8a80df07e 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
@@ -95,7 +95,7 @@ table {
           }
         ]
         [ { "decomposed extended computation" * } {
-             [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ]
+             [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxprs_dxprs" * ]
           }
         ]
         [ { "weakly normalizing computation" * } {
@@ -163,17 +163,19 @@ table {
    class "green"
    [ { "unwind" * } {
         [ { "iterated stratified static type assignment" * } {
-             [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_lsubss" + "sstas_sstas" * ]
+             [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_sstas" * ]
           }
         ]
      }
    ]
    class "grass"
    [ { "static typing" * } {
-        [ { "local env. ref. for stratified static type assignment" * } {
+(*        
+	[ { "local env. ref. for stratified static type assignment" * } {
              [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
           }
         ]
+*)
         [ { "stratified static type assignment" * } {
              [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ]
           }