X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_length.ma;h=10cc0f5798a38b16b405917c6ac79cf152a47376;hb=42705ef31dd3513a998533e02b5f20fb38dd4fb2;hp=546485cb5ab7b6292a4ec8b987fef3a9a1cda26f;hpb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
index 546485cb5..10cc0f579 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_length.ma".
+include "basic_2/syntax/lenv_length.ma".
 include "basic_2/relocation/drops.ma".
 
 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
@@ -31,13 +31,13 @@ theorem drops_fwd_length_eq1: ∀b1,b2,f,L1,K1. ⬇*[b1, f] L1 ≡ K1 →
 #b1 #b2 #f #L1 #K1 #HLK1 elim HLK1 -f -L1 -K1
 [ #f #_ #L2 #K2 #HLK2 #H lapply (length_inv_zero_sn … H) -H
   #H destruct elim (drops_inv_atom1 … HLK2) -HLK2 //
-| #f #I1 #L1 #K1 #V1 #_ #IH #X2 #K2 #HX #H elim (length_inv_succ_sn … H) -H
-  #I2 #L2 #V2 #H12 #H destruct lapply (drops_inv_drop1 … HX) -HX
+| #f #I1 #L1 #K1 #_ #IH #X2 #K2 #HX #H elim (length_inv_succ_sn … H) -H
+  #I2 #L2 #H12 #H destruct lapply (drops_inv_drop1 … HX) -HX
   #HLK2 @(IH … HLK2 H12) (**) (* auto fails *)
-| #f #I1 #L1 #K1 #V1 #V2 #_ #_ #IH #X2 #Y2 #HX #H elim (length_inv_succ_sn … H) -H
-  #I2 #L2 #V2 #H12 #H destruct elim (drops_inv_skip1 … HX) -HX
-  #K2 #W2 #HLK2 #_ #H destruct
-  lapply (IH … HLK2 H12) -f /2 width=1 by/ (**) (* full auto fails *)
+| #f #I1 #I2 #L1 #K1 #_ #_ #IH #X2 #Y2 #HX #H elim (length_inv_succ_sn … H) -H
+  #I2 #L2 #H12 #H destruct elim (drops_inv_skip1 … HX) -HX
+  #I2 #K2 #HLK2 #_ #H destruct
+  lapply (IH … HLK2 H12) -f >length_bind >length_bind /2 width=1 by/ (**) (* full auto fails *)
 ]
 qed-.  
 
@@ -47,8 +47,8 @@ lemma drops_fwd_fcla: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 →
                       ∃∃n. 𝐂⦃f⦄ ≡ n & |L1| = |L2| + n.
 #f #L1 #L2 #H elim H -f -L1 -L2
 [ /4 width=3 by fcla_isid, ex2_intro/
-| #f #I #L1 #L2 #V #_ * /3 width=3 by fcla_next, ex2_intro, eq_f/
-| #f #I #L1 #L2 #V1 #V2 #_ #_ * /3 width=3 by fcla_push, ex2_intro/
+| #f #I #L1 #L2 #_ * >length_bind /3 width=3 by fcla_next, ex2_intro, eq_f/
+| #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by fcla_push, ex2_intro/
 ]
 qed-.
 
@@ -56,7 +56,7 @@ qed-.
 lemma drops_fcla_fwd: ∀f,L1,L2,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n →
                       |L1| = |L2| + n.
 #f #l1 #l2 #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
-#m #Hm #H <(fcla_mono … Hm … Hn) -f //
+#k #Hm #H <(fcla_mono … Hm … Hn) -f //
 qed-.
 
 lemma drops_fwd_fcla_le2: ∀f,L1,L2. ⬇*[Ⓣ, f] L1 ≡ L2 →
@@ -68,21 +68,21 @@ qed-.
 lemma drops_fcla_fwd_le2: ∀f,L1,L2,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n →
                           n ≤ |L1|.
 #f #L1 #L2 #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
-#m #Hm #H <(fcla_mono … Hm … Hn) -f //
+#k #Hm #H <(fcla_mono … Hm … Hn) -f //
 qed-.
 
-lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2,V2. ⬇*[Ⓣ, f] L1 ≡ K2.ⓑ{I2}V2 →
+lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2. ⬇*[Ⓣ, f] L1 ≡ K2.ⓘ{I2} →
                           ∃∃n. 𝐂⦃f⦄ ≡ n & n < |L1|.
-#f #L1 #I2 #K2 #V2 #H elim (drops_fwd_fcla … H) -H
+#f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H
 #n #Hf #H >H -L1 /3 width=3 by le_S_S, ex2_intro/
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_lt2 *)
-lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,V2,n.
-                          ⬇*[Ⓣ, f] L1 ≡ K2.ⓑ{I2}V2 → 𝐂⦃f⦄ ≡ n →
+lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,n.
+                          ⬇*[Ⓣ, f] L1 ≡ K2.ⓘ{I2} → 𝐂⦃f⦄ ≡ n →
                           n < |L1|.
-#f #L1 #I2 #K2 #V2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
-#m #Hm #H <(fcla_mono … Hm … Hn) -f //
+#f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
+#k #Hm #H <(fcla_mono … Hm … Hn) -f //
 qed-.
 
 (* Basic_2A1: includes: drop_fwd_length_lt4 *)