X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts_vector.ma;h=62af6ac90ca762e0090018eb5e3dddb8f2f0678d;hb=42705ef31dd3513a998533e02b5f20fb38dd4fb2;hp=26d395f19fc833ba9dadb90596e8b798816106de;hpb=09b4420070d6a71990e16211e499b51dbb0742cb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
index 26d395f19..62af6ac90 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
@@ -25,10 +25,10 @@ inductive liftsv (f:rtmap): relation (list term) ≝
                liftsv f (T1 @ T1s) (T2 @ T2s)
 .
 
-interpretation "uniform relocation (vector)"
+interpretation "uniform relocation (term vector)"
    'RLiftStar i T1s T2s = (liftsv (uni i) T1s T2s).
 
-interpretation "generic relocation (vector)"
+interpretation "generic relocation (term vector)"
    'RLiftStar f T1s T2s = (liftsv f T1s T2s).
 
 (* Basic inversion lemmas ***************************************************)
@@ -122,4 +122,16 @@ lemma lifts_applv: ∀f:rtmap. ∀V1s,V2s. ⬆*[f] V1s ≡ V2s →
 #f #V1s #V2s #H elim H -V1s -V2s /3 width=1 by lifts_flat/
 qed.
 
+lemma liftsv_split_trans: ∀f,T1s,T2s. ⬆*[f] T1s ≡ T2s →
+                          ∀f1,f2. f2 ⊚ f1 ≡ f →
+                          ∃∃Ts. ⬆*[f1] T1s ≡ Ts & ⬆*[f2] Ts ≡ T2s.
+#f #T1s #T2s #H elim H -T1s -T2s
+[ /2 width=3 by liftsv_nil, ex2_intro/
+| #T1s #T2s #T1 #T2 #HT12 #_ #IH #f1 #f2 #Hf
+  elim (IH … Hf) -IH
+  elim (lifts_split_trans … HT12 … Hf) -HT12 -Hf
+  /3 width=5 by liftsv_cons, ex2_intro/
+]
+qed-.
+
 (* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)