- lambda_delta: we updated some notation

[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 29759fe08806ebc0a51ca3633218d880686d0d0f..c1666966147fdc00abb32139f41320dd24df6d9a 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -141,6 +141,12 @@ lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
 #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
+lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e.
+                     ⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d →
+                     ⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) // /2 width=1/
+qed.
+
 lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
 #L elim L -L
 [ #i #H elim (lt_zero_false … H)
@@ -194,7 +200,7 @@ lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
 ]
 qed-.
 
-lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
+lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
 [ /2 width=3/
 | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
@@ -203,7 +209,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
 qed-. 
 
 lemma ldrop_pair2_fwd_cw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
-                          ∀T. #[K, V] < #[L, T].
+                          ∀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/