X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts_lifts_vector.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts_lifts_vector.ma;h=6093315abe83662f3d7bde7b7bdd7c77c73bc2c3;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=a83fa3590ac94e36094a52e711d6b24ac04cc787;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
index a83fa3590..6093315ab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
@@ -20,9 +20,9 @@ include "basic_2/relocation/lifts_vector.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: includes: lifts_inj *)
-theorem liftsv_inj: ∀T1s,Us,f. ⬆*[f] T1s ≡ Us →
+theorem liftsv_inj: ∀f,T1s,Us. ⬆*[f] T1s ≡ Us →
                     ∀T2s. ⬆*[f] T2s ≡ Us → T1s = T2s.
-#T1s #Us #f #H elim H -T1s -Us
+#f #T1s #Us #H elim H -T1s -Us
 [ #T2s #H >(liftsv_inv_nil2 … H) -H //
 | #T1s #Us #T1 #U #HT1U #_ #IHT1Us #X #H destruct
   elim (liftsv_inv_cons2 … H) -H #T2 #T2s #HT2U #HT2Us #H destruct
@@ -31,9 +31,9 @@ theorem liftsv_inj: ∀T1s,Us,f. ⬆*[f] T1s ≡ Us →
 qed-.
 
 (* Basic_2A1: includes: liftv_mono *)
-theorem liftsv_mono: ∀Ts,U1s,f. ⬆*[f] Ts ≡ U1s →
+theorem liftsv_mono: ∀f,Ts,U1s. ⬆*[f] Ts ≡ U1s →
                      ∀U2s. ⬆*[f] Ts ≡ U2s → U1s = U2s.
-#Ts #U1s #f #H elim H -Ts -U1s
+#f #Ts #U1s #H elim H -Ts -U1s
 [ #U2s #H >(liftsv_inv_nil1 … H) -H //
 | #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct
   elim (liftsv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct
@@ -43,9 +43,9 @@ qed-.
 
 (* Basic_1: includes: lifts1_xhg (right to left) *)
 (* Basic_2A1: includes: liftsv_liftv_trans_le *)
-theorem liftsv_trans: ∀T1s,Ts,f1. ⬆*[f1] T1s ≡ Ts → ∀T2s,f2. ⬆*[f2] Ts ≡ T2s →
+theorem liftsv_trans: ∀f1,T1s,Ts. ⬆*[f1] T1s ≡ Ts → ∀T2s,f2. ⬆*[f2] Ts ≡ T2s →
                       ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1s ≡ T2s.
-#T1s #Ts #f1 #H elim H -T1s -Ts
+#f1 #T1s #Ts #H elim H -T1s -Ts
 [ #T2s #f2 #H >(liftsv_inv_nil1 … H) -T2s /2 width=3 by liftsv_nil/
 | #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #f2 #H elim (liftsv_inv_cons1 … H) -H
   #T2 #T2s #HT2 #HT2s #H destruct /3 width=6 by lifts_trans, liftsv_cons/