From de64015de66a48373ade6cab7508d8f8e2c43af9 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 19 Apr 2012 13:06:00 +0000
Subject: [PATCH] - firs theorems on native type assignment - we removed
 iterated unfold on local environments   since transitivity of this unfold is
 not needed so far

---
 .../contribs/lambda_delta/basic_2/basic_1.txt |   8 -
 .../basic_2/computation/cprs_lcpr.ma          |   2 +-
 .../basic_2/equivalence/lcpcs_lcpcs.ma        |   4 +-
 .../ltpsss/aaa_ltpsss.etc}                    |   0
 .../ltpsss/cpr_ltpsss.etc}                    |   0
 .../basic_2/etc/ltpsss/cprs_lcpr.etc          |  46 ++++
 .../lambda_delta/basic_2/etc/ltpsss/lcpr.etc  |  37 ++++
 .../basic_2/etc/ltpsss/lcpr_aaa.etc           |  34 +++
 .../basic_2/etc/ltpsss/lcpr_cpr.etc           |  27 +++
 .../basic_2/etc/ltpsss/lcpr_lcpr.etc          |  40 ++++
 .../ltpsss/ltpr_ltpsss.etc}                   |   0
 .../ltpsss.ma => etc/ltpsss/ltpsss.etc}       |   0
 .../ltpsss/ltpsss_ldrop.etc}                  |   0
 .../ltpsss/ltpsss_ltpsss.etc}                 |   0
 .../ltpsss/ltpsss_tps.etc}                    |   0
 .../ltpsss/ltpsss_tpss.etc}                   |   0
 .../basic_2/etc/ltpsss/notation.etc           |  21 ++
 .../lambda_delta/basic_2/grammar/aarity.ma    |  12 +-
 .../lambda_delta/basic_2/native/nta.ma        |  51 +++++
 .../lambda_delta/basic_2/native/nta_lift.ma   | 201 ++++++++++++++++++
 .../contribs/lambda_delta/basic_2/notation.ma |  14 +-
 .../lambda_delta/basic_2/reducibility/lcpr.ma |   6 +-
 .../basic_2/reducibility/lcpr_aaa.ma          |   2 +-
 .../basic_2/reducibility/lcpr_cpr.ma          |   4 +-
 .../basic_2/reducibility/lcpr_lcpr.ma         |  14 +-
 .../lambda_delta/basic_2/static/sh.ma         |   2 +-
 .../basic_2/substitution/lift_lift.ma         |   2 +-
 27 files changed, 492 insertions(+), 35 deletions(-)
 rename matita/matita/contribs/lambda_delta/basic_2/{static/aaa_ltpsss.ma => etc/ltpsss/aaa_ltpsss.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{reducibility/cpr_ltpsss.ma => etc/ltpsss/cpr_ltpsss.etc} (100%)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc
 rename matita/matita/contribs/lambda_delta/basic_2/{reducibility/ltpr_ltpsss.ma => etc/ltpsss/ltpr_ltpsss.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{unfold/ltpsss.ma => etc/ltpsss/ltpsss.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{unfold/ltpsss_ldrop.ma => etc/ltpsss/ltpsss_ldrop.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{unfold/ltpsss_ltpsss.ma => etc/ltpsss/ltpsss_ltpsss.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{unfold/ltpsss_tps.ma => etc/ltpsss/ltpsss_tps.etc} (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{unfold/ltpsss_tpss.ma => etc/ltpsss/ltpsss_tpss.etc} (100%)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/native/nta.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index caa897dec..92bd9860d 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -242,11 +242,7 @@ ty3/dec ty3_inference
 ty3/fsubst0 ty3_fsubst0
 ty3/fsubst0 ty3_csubst0
 ty3/fsubst0 ty3_subst0
-ty3/fwd ty3_gen_sort
-ty3/fwd ty3_gen_lref
-ty3/fwd ty3_gen_bind
 ty3/fwd ty3_gen_appl
-ty3/fwd ty3_gen_cast
 ty3/fwd tys3_gen_nil
 ty3/fwd tys3_gen_cons
 ty3/fwd_nf2 ty3_gen_appl_nf2
@@ -271,12 +267,8 @@ ty3/pr3_props ty3_tred
 ty3/pr3_props ty3_sconv_pc3
 ty3/pr3_props ty3_sred_back
 ty3/pr3_props ty3_sconv
-ty3/props ty3_lift
-ty3/props ty3_correct
 ty3/props ty3_unique
 ty3/props ty3_gen_abst_abst
-ty3/props ty3_typecheck
-ty3/props ty3_getl_subst0
 ty3/sty0 ty3_sty0
 ty3/subst1 ty3_gen_cabbr
 ty3/subst1 ty3_gen_cvoid
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma
index bb7896c30..14bcfd5c4 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/reducibility/ltpr_tps.ma".
-include "basic_2/reducibility/cpr_ltpsss.ma".
+include "basic_2/reducibility/cpr_ltpss.ma".
 include "basic_2/reducibility/lcpr.ma".
 include "basic_2/computation/cprs.ma".
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma
index cc26a5647..876161bd2 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_lcpcs.ma
@@ -44,7 +44,7 @@ theorem lcpcs_trans: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢
 /2 width=3/ qed.
 
 theorem lcpcs_canc_sn: ∀L,L1,L2. L ⊢ ⬌* L1 → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
-/3 width=3/ qed.
+/3 width=3 by lcpcs_trans, lcprs_comm/ qed.
 
 theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* L2.
-/3 width=3/ qed.
+/3 width=3 by lcpcs_trans, lcprs_comm/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpsss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/aaa_ltpsss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpsss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cpr_ltpsss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc
new file mode 100644
index 000000000..bb7896c30
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/cprs_lcpr.etc
@@ -0,0 +1,46 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reducibility/ltpr_tps.ma".
+include "basic_2/reducibility/cpr_ltpsss.ma".
+include "basic_2/reducibility/lcpr.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties concerning context-sensitive parallel reduction on lenv's *****)
+
+lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 →
+                       ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2
+[ /2 width=3/
+| #T #T2 #_ #HT2 * #T0 #HT10 #HT0
+  elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32
+  @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *)
+  @(cprs_strap1 … T3 …) /2 width=1/ -HT32
+  @(cprs_strap1 … HT0) -HT0 /3 width=3/
+]
+qed.
+
+(* Basic_1: was just: pr3_pr0_pr2_t *)
+lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 * #T #HT1
+<(ltpr_fwd_length … HL12) #HT2
+elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/
+qed.
+
+(* Basic_1: was just: pr3_pr2_pr2_t *)
+lemma lcpr_cpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 * /3 width=7/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc
new file mode 100644
index 000000000..4d8a341bc
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr.etc
@@ -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/unfold/ltpsss.ma".
+include "basic_2/reducibility/ltpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+definition lcpr: relation lenv ≝
+   λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶** L2
+.
+
+interpretation
+  "context-sensitive parallel reduction (environment)"
+  'CPRed L1 L2 = (lcpr L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lcpr_refl: ∀L. L ⊢ ➡ L.
+/2 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 //
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc
new file mode 100644
index 000000000..77f384e58
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_aaa.etc
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/aaa_ltpsss.ma".
+include "basic_2/reducibility/ltpr_aaa.ma".
+include "basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ÷ A.
+#L1 #T #A #HT #L2 * /3 width=5/
+qed.
+
+lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ÷ A.
+#L #T1 #A #HT1 #T2 * /3 width=5/
+qed.
+
+lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡ L2 →
+                         ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+/3 width=3/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc
new file mode 100644
index 000000000..3d833fc02
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_cpr.etc
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltpsss_ltpsss.ma".
+include "basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+(* Advanced properties ****************************************************)
+
+lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 →
+                 ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2.
+#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
+<(ltpsss_fwd_length … HL2) /4 width=5/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc
new file mode 100644
index 000000000..5d7e4739e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/lcpr_lcpr.etc
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltpsss_ltpsss.ma".
+include "basic_2/reducibility/ltpr_ltpsss.ma".
+include "basic_2/reducibility/ltpr_ltpr.ma".
+include "basic_2/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***************)
+
+(* Main properties **********************************************************)
+
+theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 →
+                   ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L.
+#K0 #L1 #L2 * #K1 #HK01 #HKL1 * #K2 #HK02 #HKL2
+lapply (ltpr_fwd_length … HK01) #H
+>(ltpr_fwd_length … HK02) in H; #H
+elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2
+lapply (ltpsss_fwd_length … HKL1) #H1
+lapply (ltpsss_fwd_length … HKL2) #H2
+>H1 in HKL1 H; -H1 #HKL1
+>H2 in HKL2; -H2 #HKL2 #H
+elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
+elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
+elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2
+lapply (ltpr_fwd_length … HLK1) #H1
+lapply (ltpr_fwd_length … HLK2) #H2
+/3 width=5/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpsss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpr_ltpsss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ldrop.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ldrop.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_ltpsss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_ltpsss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tps.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tpss.ma
rename to matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/ltpsss_tpss.etc
diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc
new file mode 100644
index 000000000..6846b7670
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/ltpsss/notation.etc
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 λδ ****************************************)
+
+(* Unfold *******************************************************************)
+
+notation "hvbox( T1 break [ d , break e ] ▶** break T2 )"
+   non associative with precedence 45
+   for @{ 'PSubstStars $T1 $d $e $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma
index f71f2d62e..0d7db6beb 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma
@@ -12,13 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
- * Support for abstract candidates of reducibility closed: 2012 January 27
- * Confluence of context-sensitive parallel reduction closed: 2011 September 21
- * Confluence of context-free parallel reduction closed: 2011 September 6
- * Specification started: 2011 April 17
+(* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES
  * - Patience on me to gain peace and perfection! -
  * [ suggested invocation to start formal specifications with ]
+ * Context-sensitive subject equivalence for atomic arity assignment: 2012 April 16
+ * Context-sensitive strong normalization for simply typed terms: 2012 March 15
+ * Support for abstract candidates of reducibility closed: 2012 January 27
+ * Confluence for context-sensitive parallel reduction: 2011 September 21
+ * Confluence for context-free parallel reduction: 2011 September 6
+ * Specification starts: 2011 April 17
  *)
 
 include "ground_2/star.ma".
diff --git a/matita/matita/contribs/lambda_delta/basic_2/native/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/native/nta.ma
new file mode 100644
index 000000000..99592cdd9
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/native/nta.ma
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/sh.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+inductive nta (h:sh): lenv → relation term ≝
+| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k))
+| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
+            ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
+            ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U →
+            nta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| nta_appl: ∀L,V,W,U,T1,T2. nta h L V W → nta h L W U → nta h (L.ⓛW) T1 T2 →
+            nta h L (ⓐV.ⓛW.T1) (ⓐV.ⓛW.T2)
+| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
+            nta h L (ⓐV.T) (ⓐV.U)
+| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U
+| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
+            nta h L T U2
+.
+
+interpretation "native type assignment (term)"
+   'NativeType h L T U = (nta h L T U).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: ty3_cast *)
+lemma nta_cast_old: ∀h,L,W,T,U.
+                    ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓣU.T : ⓣW.U.
+/4 width=3/ qed.
+
+(* Basic_1: was: ty3_typecheck *)
+lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0.
+/3 width=2/ qed.
+
+(* Basic_1: removed theorems 1: ty3_getl_subst0 *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma
new file mode 100644
index 000000000..6e9d1b2a2
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma
@@ -0,0 +1,201 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/native/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+fact nta_inv_sort_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
+                       L ⊢ ⋆(next h k0) ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #k0 #H destruct //
+| #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #k0 #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
+| #L #T #U #_ #_ #k0 #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
+  lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0
+  lapply (cpcs_trans … Hk0 … HU12) -U1 //
+]
+qed.
+
+(* Basic_1: was: ty3_gen_sort *)
+lemma nta_inv_sort: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
+/2 width=3/ qed-.
+
+fact nta_inv_lref_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
+                       (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+                                    ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                       ) ∨
+                       (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+                                    ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                       ).
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #j #H destruct
+| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
+| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
+| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #j #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #T #U #_ #_ #j #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
+  elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
+  lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
+]
+qed.
+
+(* Basic_1: was ty3_gen_lref *)
+lemma nta_inv_lref: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
+                    (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+                                 ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                    ) ∨
+                    (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+                                 ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                    ).
+/2 width=3/ qed-.
+
+fact nta_inv_bind_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
+                       ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+                                L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U #_ #_ #J #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
+  elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+(* Basic_1: was: ty3_gen_bind *)
+lemma nta_inv_bind: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
+                    ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+                             L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+/2 width=3/ qed-.                            
+
+fact nta_inv_cast_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
+                    ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+  elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
+]
+qed.
+
+(* Basic_1: was: ty3_gen_cast *)
+lemma nta_inv_cast: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+/2 width=3/ qed-.
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: ty3_lift *)
+lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+                ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  >(lift_inv_sort1 … H1) -X1
+  >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+    /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+    lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+    elim (lift_total V1 (d-i-1) e) /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct
+  elim (lift_total W1 d e) /4 width=6/
+| #L1 #V1 #W1 #U1 #T11 #T12 #_ #_ #_ #IHVW1 #IHWU1 #IHT112 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
+  elim (lift_inv_bind1 … H1) -H1 #W2 #T12 #HW12 #HT112 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #X0 #X #H0 #H2 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #Y0 #T22 #H2 #HT122 #H destruct
+  lapply (lift_mono … H0 … HV12) -H0 #H destruct
+  lapply (lift_mono … H2 … HW12) -H2 #H destruct
+  elim (lift_total U1 d e) #U2 #HU12
+  @nta_appl [2,3: /2 width=5/ | skip | /3 width=5/ ] (**) (* explicit constructor, /4 width=6/ is too slow *)
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct
+  elim (lift_total W1 d e) /4 width=6/
+| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+  elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+  lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
+| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
+  elim (lift_total U11 d e) #U #HU11
+  elim (lift_total V12 d e) #V22 #HV122
+  lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+(* Basic_1: was: ty3_correct *)
+lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=2/
+| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
+| #L #V #W #U #T1 #T2 #HVW #HWU #_ #_ #_ * /3 width=2/
+| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
+| #L #T #U #_ * /2 width=2/
+| /2 width=2/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was: ty3_appl *)
+lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U →
+                    ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
+#h #L #V #W #T #U #HVW #HTU
+elim (nta_fwd_correct … HTU) #X #H
+elim (nta_inv_bind … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index d8ab202ff..7be9b8ecb 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -184,10 +184,6 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ▶▶* break T2 )
    non associative with precedence 45
    for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
 
-notation "hvbox( T1 break [ d , break e ] ▶** break T2 )"
-   non associative with precedence 45
-   for @{ 'PSubstStars $T1 $d $e $T2 }.
-
 notation "hvbox( T1 break [ d , break e ] ≡ break T2 )"
    non associative with precedence 45
    for @{ 'TSubst $T1 $d $e $T2 }.
@@ -325,3 +321,13 @@ notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )"
 notation "hvbox( T1 ⊢ ⬌* break T2 )"
    non associative with precedence 45
    for @{ 'CPConvStar $T1 $T2 }.
+
+(* Native typing ************************************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 : break T2 )"
+   non associative with precedence 45
+   for @{ 'NativeType $h $L $T1 $T2 }.
+
+notation "hvbox( h ⊢ break term 90 L1 : ⊑ break L2 )"
+   non associative with precedence 45
+   for @{ 'CrSubEqN $h $L1 $L2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma
index 4d8a341bc..51028c240 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma
@@ -12,13 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/ltpsss.ma".
+include "basic_2/unfold/ltpss.ma".
 include "basic_2/reducibility/ltpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
 
 definition lcpr: relation lenv ≝
-   λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶** L2
+   λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶* L2
 .
 
 interpretation
@@ -33,5 +33,5 @@ lemma lcpr_refl: ∀L. L ⊢ ➡ L.
 (* Basic inversion lemmas ***************************************************)
 
 lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
-#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 //
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
 qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma
index 77f384e58..61ed86b5b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/static/aaa_ltpsss.ma".
+include "basic_2/static/aaa_ltpss.ma".
 include "basic_2/reducibility/ltpr_aaa.ma".
 include "basic_2/reducibility/cpr.ma".
 include "basic_2/reducibility/lcpr.ma".
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma
index 3d833fc02..08f63e87f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/ltpsss_ltpsss.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
 include "basic_2/reducibility/cpr.ma".
 include "basic_2/reducibility/lcpr.ma".
 
@@ -23,5 +23,5 @@ include "basic_2/reducibility/lcpr.ma".
 lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 →
                  ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2.
 #L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
-<(ltpsss_fwd_length … HL2) /4 width=5/
+<(ltpss_fwd_length … HL2) /4 width=5/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma
index 5d7e4739e..2b1f4a4fd 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/ltpsss_ltpsss.ma".
-include "basic_2/reducibility/ltpr_ltpsss.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/reducibility/ltpr_ltpss.ma".
 include "basic_2/reducibility/ltpr_ltpr.ma".
 include "basic_2/reducibility/lcpr.ma".
 
@@ -27,13 +27,13 @@ theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 →
 lapply (ltpr_fwd_length … HK01) #H
 >(ltpr_fwd_length … HK02) in H; #H
 elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2
-lapply (ltpsss_fwd_length … HKL1) #H1
-lapply (ltpsss_fwd_length … HKL2) #H2
+lapply (ltpss_fwd_length … HKL1) #H1
+lapply (ltpss_fwd_length … HKL2) #H2
 >H1 in HKL1 H; -H1 #HKL1
 >H2 in HKL2; -H2 #HKL2 #H
-elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
-elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
-elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2
+elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
+elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
+elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2
 lapply (ltpr_fwd_length … HLK1) #H1
 lapply (ltpr_fwd_length … HLK2) #H2
 /3 width=5/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
index 4eeac01b8..0577b0015 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma
@@ -16,7 +16,7 @@ include "ground_2/arith.ma".
 
 (* SORT HIERARCHY ***********************************************************)
 
-(* sort hierarchy specifications *)
+(* sort hierarchy specification *)
 record sh: Type[0] ≝ {
    next: nat → nat;        (* next sort in the hierarchy *)
    next_lt: ∀k. k < next k (* strict monotonicity condition *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma
index 74edd2ea2..e70389973 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma
@@ -69,7 +69,7 @@ theorem lift_div_le: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T →
 ]
 qed.
 
-(* Note: apparently this was missing in Basic_1 *)
+(* Note: apparently this was missing in basic_1 *)
 theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T →
                      ∀e,e2,T2. ⇧[d1 + e, e2] T2 ≡ T →
                      e ≤ e1 → e1 ≤ e + e2 →
-- 
2.39.2