X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts_vector.ma;h=8acd0a571249d2c4332d87ccbaf016c589c53a22;hb=9be6753b7f120a4222df17d1116fe91e871f9367;hp=26d395f19fc833ba9dadb90596e8b798816106de;hpb=5712c83e9c25c8cf44812586c31ee823771e95e0;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..8acd0a571 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
@@ -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 *)