From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 4 Jun 2012 20:34:11 +0000 (+0000)
Subject: - lambda_delta: subject reduction for nativa type assignment begins ...
X-Git-Tag: make_still_working~1661
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fde3b3d2e6cc48f6c9880136b1a0d565e2c78c1f;p=helm.git

- lambda_delta: subject reduction for nativa type assignment begins ...
                dependecnes between source files improved
- matitadep: little application for optimizing dependences between .ma files
             (used by lambda_delta Makefile)
---

diff --git a/matita/components/binaries/matitadep/Makefile b/matita/components/binaries/matitadep/Makefile
new file mode 100644
index 000000000..7695ab288
--- /dev/null
+++ b/matita/components/binaries/matitadep/Makefile
@@ -0,0 +1,6 @@
+EXEC = matitadep
+VERSION=0.1.0
+
+REQUIRES =
+
+include ../Makefile.common
diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml
new file mode 100644
index 000000000..ebb87695f
--- /dev/null
+++ b/matita/components/binaries/matitadep/matitadep.ml
@@ -0,0 +1,47 @@
+module StringSet = Set.Make (String) 
+
+type file = {
+   ddeps: string list;
+   rdeps: StringSet.t option
+}
+
+let graph = Hashtbl.create 503
+
+let add fname =
+   if Hashtbl.mem graph fname then () else
+   Hashtbl.add graph fname {ddeps = []; rdeps = None}
+
+let add_ddep fname dname =
+   let file = Hashtbl.find graph fname in
+   Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps} 
+
+let init fname dname =
+   add fname; add dname; add_ddep fname dname 
+
+let rec compute fname file = match file.rdeps with
+   | Some rdeps -> rdeps
+   | None       ->
+      let rdeps = List.fold_left (iter fname) StringSet.empty file.ddeps in
+      Hashtbl.replace graph fname {file with rdeps = Some rdeps};
+      rdeps
+
+and iter fname rdeps dname =
+   if StringSet.mem dname rdeps then
+      begin Printf.printf "%s: redundant %s\n" fname dname; rdeps end
+   else
+     let file = Hashtbl.find graph dname in
+     StringSet.add dname (StringSet.union (compute dname file) rdeps)
+
+let check () = 
+   let iter fname file = 
+      if StringSet.mem fname (compute fname file) then
+         Printf.printf "%s: circular\n" fname 
+   in
+   Hashtbl.iter iter graph 
+
+let rec read ich = 
+   let _ = Scanf.fscanf ich "./%s@:include \"%s@\". " init in
+   read ich
+   
+let _ =
+   try read stdin with End_of_file -> check ()
diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile
index 71dff0f41..964277d7f 100644
--- a/matita/matita/contribs/lambda_delta/Makefile
+++ b/matita/matita/contribs/lambda_delta/Makefile
@@ -1,6 +1,8 @@
 H        = @
 XOA_DIR  = ../../../components/binaries/xoa
 XOA      = xoa.native
+DEP_DIR  = ../../../components/binaries/matitadep
+DEP      = matitadep.native
 
 CONF     = ground_2/xoa.conf.xml
 TARGETS  = ground_2/xoa_natation.ma ground_2/xoa.ma
@@ -27,6 +29,14 @@ orig: $(ORIGS)
 	@echo "  ORIG basic_2"
 	$(H)$(ORIG) basic_2 < $(ORIGS)
 
+# dep ########################################################################
+
+deps: MAS = $(shell find $* -name "*.ma")
+
+deps: $(DEP_DIR)/$(DEP)
+	@echo "  MATITADEP"
+	$(H)grep "include \"" $(MAS) | $<
+
 # stats ######################################################################
 
 stats: $(PACKAGES:%=%.stats)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
index 14b516624..3965d1619 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma
@@ -13,12 +13,18 @@
 (**************************************************************************)
 
 include "basic_2/reducibility/cpr_delift.ma".
+include "basic_2/reducibility/cpr_cpr.ma".
 include "basic_2/computation/cprs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
 
 (* Properties on inverse basic term relocation ******************************)
 
+lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 → L ⊢ ⓓV.T1 ➡* T2.
+#L #V #T1 #T2 * #T #HT1 #HT2
+@(cprs_strap2 … (ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *)
+qed.
+
 (* Basic_1: was only: pr3_gen_cabbr *)
 lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
                              ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
index c9b39fce3..6b5889327 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reducibility/cpr.ma".
 include "basic_2/reducibility/cnf.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma
index e9f8062c8..a7c7c7a99 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/static/aaa_lift.ma".
-include "basic_2/computation/acp_cr.ma".
 include "basic_2/computation/lsubc.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
new file mode 100644
index 000000000..6ecc0bb81
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
@@ -0,0 +1,179 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/nta_ltpss.ma".
+include "basic_2/dynamic/nta_thin.ma".
+include "basic_2/dynamic/lsubn_nta.ma".
+
+lemma cpr_beta: ∀L,V1,V2,W,T1,T2.
+                V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
+#L #V1 #V2 #W #T1 #T2 #HV12 * #T #HT1 #HT2
+lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
+lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+@(ex2_1_intro … (ⓓV2.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *)
+qed.
+
+lemma cpr_beta2: ∀L,V1,V2,W,T1,T2.
+                 L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
+#L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2
+lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
+lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+@(ex2_1_intro … (ⓓV.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *)
+qed.
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties on context-free parallel reduction for local environments ******)
+
+lemma nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
+                         ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
+#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
+[ #L1 #k #L2 #_ #T2 #H
+  >(tpr_inv_atom1 … H) -H //
+| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H
+  >(tpr_inv_atom1 … H) -T2
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
+  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
+| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H
+  >(tpr_inv_atom1 … H) -T2
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
+  elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
+  lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
+  elim (lift_total V1 0 (i+1)) #W #HW
+  lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW
+  elim (lift_total W2 0 (i+1)) #U2 #HWU2
+  lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12
+  @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *)
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
+  elim (tpr_inv_bind1 … H) -H *
+  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
+    lapply (IHVW1 … HL12 … HV12) #HV2W1
+    lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1
+    lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1
+    lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H
+    lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
+    lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1
+    elim (nta_fwd_correct … H) -H #U2 #HU12
+    @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *)
+  | #T #HT1 #HTX #H destruct
+    lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1
+    elim (lift_total X 0 1) #Y #HXY
+    lapply (tpr_lift … HTX … HT1 … HXY) -T #H
+    lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H
+    elim (nta_fwd_correct … H) #T1 #HUT1
+    elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H
+    normalize in ⊢ (??%??? → ?); #HU1
+    lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct
+    @(nta_conv … U) // /2 width=2/
+  ]
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
+  elim (tpr_inv_appl1 … H) -H *
+  [ #V2 #Y #HV12 #HY #H destruct
+    elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
+    lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H
+    elim (nta_fwd_correct … H) -H #X #H
+    elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_
+    @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+  | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
+    lapply (IHVW1 … HL12 … HV12) #HVW2
+    lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2
+    lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1
+    elim (nta_fwd_correct … H1) #T #H2
+    elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
+    elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
+    elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0 
+    lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
+    @(nta_conv … (ⓓV2.U2))
+    [2: /2 width=2/
+    |3: -h -L1 -T0 -T2 -W -U0
+    |4: /3 width=2/ 
+    ]
+  | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
+  ]
+
+
+
+
+
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  lapply (cpr_tpss … HV12) #HV
+  elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU
+  @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
+  elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
+  lapply (cpr_tpss … HU12) /4 width=4/
+| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
+  @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
+]
+qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
+                            ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
+  
+  
+| #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
+  elim (tpr_inv_appl1 … H) -H *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
+    lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/
+  | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
+    elim (nta_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
+    lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
+    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
+  | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
+    elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
+    lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
+    lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
+    lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
+    @(nta_abbr … HW2) -HW2
+    @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
+  ]
+| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
+  elim (tpr_inv_cast1 … H) -H
+  [ * #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
+    lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
+  | -HV1 #HT1X
+     lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
+  ]
+]
+qed.
+
+/2 width=9/ qed.
+
+lemma nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
+/2 width=5/ qed.
+
+lemma nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
+/2 width=5/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
index 1fb994c71..7394858ef 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma
@@ -24,11 +24,17 @@ lemma cpcs_cprs_dx: ∀L,T1,T2. L ⊢ T1 ➡* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /3 width=3/
 qed.
 
+lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2.
+/3 width=1/ qed.
+
 (* Basic_1: was: pc3_pr3_x *)
 lemma cpcs_cprs_sn: ∀L,T1,T2. L ⊢ T2 ➡* T1 → L ⊢ T1 ⬌* T2.
 #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /3 width=3/
 qed.
 
+lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2.
+/3 width=1/ qed.
+
 lemma cpcs_cprs_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2.
 #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
index e57f9f32b..b812830ee 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
@@ -20,6 +20,10 @@ include "basic_2/equivalence/cpcs_cpcs.ma".
 
 (* Properties on inverse basic term relocation ******************************)
 
+lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ▼*[O, 1] ≡ T2 →
+                             L ⊢ T2 ⬌* ⓓV.T1.
+/3 width=1/ qed.
+
 (* Basic_1: was only: pc3_gen_cabbr *)
 lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 →
                              ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma
index 1bec6e57d..6dc6714a9 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_ltpss.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/ltpss_ltpss.ma".
 include "basic_2/equivalence/cpcs_cpcs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
index 072d951ba..401a4be64 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/cl_shift.ma".
 include "basic_2/unfold/tpss.ma".
 include "basic_2/reducibility/tpr.ma".
 
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 c620b4eca..50c559734 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,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_lcpr.ma
index 2b1f4a4fd..4b1f9b51a 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,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-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".
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
index d284060f1..303604958 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/cl_weight.ma".
 include "basic_2/substitution/ldrop.ma".
 
 (* PARALLEL SUBSTITUTION ON TERMS *******************************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
index a4c94fedc..f6cb1fa3f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lift_lift.ma".
 include "basic_2/unfold/tpss_tpss.ma".
 include "basic_2/unfold/delift.ma".
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
index d8c746697..a6846d3b8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
@@ -117,6 +117,13 @@ elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU
 >(lift_mono … HTU2 … HT2) -T2 /2 width=3/
 qed.
 
+lemma delift_inv_lift1_eq: ∀L,U1,T2,d,e. L ⊢ U1 ▼*[d, e] ≡ T2 →
+                           ∀K. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → T1 = T2.
+#L #U1 #T2 #d #e * #U2 #HU12 #HTU2 #K #HLK #T1 #HTU1
+lapply (tpss_inv_lift1_eq … HU12 … HTU1) -L -K #H destruct
+lapply (lift_inj … HTU1 … HTU2) -U2 //
+qed-.
+
 lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 ▼*[i, d + e - i] ≡ T →
                           ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e →
                           L ⊢ T1 ▼*[d, e] ≡ T2.