- 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 3dfc3563906caeb81ffd56ea44b0221bd07869b2..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,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_weight.ma".
+include "basic_2/grammar/cl_weight.ma".
 include "basic_2/grammar/lsubs.ma".
 include "basic_2/substitution/lift.ma".
 
@@ -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