X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_lifts.ma;h=3aef874bc1731e436318e7234529f3d340c50287;hp=971d23ac978dbc1f392b2644d17d5a9323caeebc;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
index 971d23ac9..3aef874bc 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
@@ -47,8 +47,8 @@ theorem lifts_div4: ∀f2,Tf,T. ⇧*[f2] Tf ≘ T → ∀g2,Tg. ⇧*[g2] Tg ≘
 qed-.
 
 lemma lifts_div4_one: ∀f,Tf,T. ⇧*[⫯f] Tf ≘ T →
-                      ∀T1. ⇧*[1] T1 ≘ T →
-                      ∃∃T0. ⇧*[1] T0 ≘ Tf & ⇧*[f] T0 ≘ T1.
+                      ∀T1. ⇧[1] T1 ≘ T →
+                      ∃∃T0. ⇧[1] T0 ≘ Tf & ⇧*[f] T0 ≘ T1.
 /4 width=6 by lifts_div4, at_div_id_dx, at_div_pn/ qed-.
 
 theorem lifts_div3: ∀f2,T,T2. ⇧*[f2] T2 ≘ T → ∀f,T1. ⇧*[f] T1 ≘ T →
@@ -87,8 +87,8 @@ theorem lifts_trans: ∀f1,T1,T. ⇧*[f1] T1 ≘ T → ∀f2,T2. ⇧*[f2] T ≘
 qed-.
 
 lemma lifts_trans4_one (f) (T1) (T2):
-                       ∀T. ⇧*[1]T1 ≘ T → ⇧*[⫯f]T ≘ T2 →
-                       ∃∃T0. ⇧*[f]T1 ≘ T0 & ⇧*[1]T0 ≘ T2.
+                       ∀T. ⇧[1]T1 ≘ T → ⇧*[⫯f]T ≘ T2 →
+                       ∃∃T0. ⇧*[f]T1 ≘ T0 & ⇧[1]T0 ≘ T2.
 /4 width=6 by lifts_trans, lifts_split_trans, after_uni_one_dx/ qed-.
 
 (* Basic_2A1: includes: lift_conf_O1 lift_conf_be *)
@@ -135,8 +135,8 @@ elim (HR … HU12 … HTU1) -HR -U1 #X #HUX #HTX
 qed-.
 
 lemma lifts_trans_uni (T):
-      ∀l1,T1. ⇧*[l1] T1 ≘ T →
-      ∀l2,T2. ⇧*[l2] T ≘ T2 → ⇧*[l1+l2] T1 ≘ T2.
+      ∀l1,T1. ⇧[l1] T1 ≘ T →
+      ∀l2,T2. ⇧[l2] T ≘ T2 → ⇧[l1+l2] T1 ≘ T2.
 #T #l1 #T1 #HT1 #l2 #T2 #HT2
 @(lifts_trans … HT1 … HT2) //
 qed-.