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=971d23ac978dbc1f392b2644d17d5a9323caeebc;hp=e55582cb9870f5ffe2675df88e24c41ef15d4ffa;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hpb=f38fd769279794d0ca73c8945eac30e8b42e59be

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..971d23ac9 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
@@ -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-.