(* *)
(**************************************************************************)
-include "basic_2/grammar/term_vector.ma".
+include "basic_2/syntax/term_vector.ma".
include "basic_2/relocation/lifts.ma".
(* GENERIC RELOCATION FOR TERM VECTORS *************************************)
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 ***************************************************)
#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 *)