- firs theorems on native type assignment

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / substitution / ldrop.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index c00819a7454644157340366ca2dd9e59c0f2bef8..4550fde4b9aa92f01f0da5d187acca6ec3614a82 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/lenv_weight.ma".
-include "Basic_2/grammar/lsubs.ma".
-include "Basic_2/substitution/lift.ma".
+include "basic_2/grammar/cl_weight.ma".
+include "basic_2/grammar/lsubs.ma".
+include "basic_2/substitution/lift.ma".
 
 (* LOCAL ENVIRONMENT SLICING ************************************************)
 
@@ -187,6 +187,13 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
 ]
 qed-. 
 
+lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
+                          ∀T. #[K, V] < #[L, T].
+#I #L #K #V #d #e #H #T
+lapply (ldrop_fwd_lw … H) -H #H
+@(le_to_lt_to_lt … H) -H /3 width=1/
+qed-.
+
 lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
                                ⇩[0, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
 #L1 elim L1 -L1
@@ -211,8 +218,8 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e.
 ]
 qed-.
 
-(* Basic_1: removed theorems 49:
-            drop_skip_flat
+(* Basic_1: removed theorems 50:
+            drop_ctail drop_skip_flat 
             cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
             drop_clear drop_clear_O drop_clear_S
             clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r