X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flifts_lift_vector.ma;h=ecba0fd777862290a907a0b34c32a241d39b58a4;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=559e62659ec9db7ed63134ffc03ef4de91f3e517;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
index 559e62659..ecba0fd77 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_lift_vector.ma
@@ -21,9 +21,9 @@ include "basic_2/multiple/lifts_vector.ma".
 (* Main properties **********************************************************)
 
 (* Basic_1: was: lifts1_xhg (right to left) *)
-lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
-                             ∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
-                             ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s.
+lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⬆*[des] T1s ≡ Ts →
+                             ∀T2s:list term. ⬆[0, 1] Ts ≡ T2s →
+                             ∃∃T0s. ⬆[0, 1] T1s ≡ T0s & ⬆*[des + 1] T0s ≡ T2s.
 #T1s #Ts #des #H elim H -T1s -Ts
 [ #T1s #H
   >(liftv_inv_nil1 … H) -T1s /2 width=3/