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=98fbba1b68d457807c73ebf70eb2a48696381da4;hp=7426ebb5359d0571b79f40bb4c0bd6059001a69f;hpb=65e6209e0758832835ba8d14304a1548d059a634;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 7426ebb53..10cc0f579 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
@@ -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 >length_pair >length_pair /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 #_ * >length_pair /3 width=3 by fcla_next, ex2_intro, eq_f/
-| #f #I #L1 #L2 #V1 #V2 #_ #_ * >length_pair >length_pair /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-.
 
@@ -71,17 +71,17 @@ lemma drops_fcla_fwd_le2: ∀f,L1,L2,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃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
+#f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
 #k #Hm #H <(fcla_mono … Hm … Hn) -f //
 qed-.