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

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 e55582cb9..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 *)
@@ -133,3 +133,10 @@ lemma deliftable2_sn_bi: ∀R. deliftable2_sn R → deliftable2_bi R.
 elim (HR … HU12 … HTU1) -HR -U1 #X #HUX #HTX
 <(lifts_inj … HUX … HTU2) -U2 -T2 -f //
 qed-.
+
+lemma lifts_trans_uni (T):
+      ∀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-.