X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_lifts.ma;h=0581f6d1c3a28dc4b3b07b25473737a83e54a537;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=41c641716a280339f1c67ae399d534dead1e23aa;hpb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;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 41c641716..0581f6d1c 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma
@@ -86,6 +86,11 @@ 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.
+/4 width=6 by lifts_trans, lifts_split_trans, after_uni_one_dx/ qed-.
+
 (* Basic_2A1: includes: lift_conf_O1 lift_conf_be *)
 theorem lifts_conf: ∀f1,T,T1. ⬆*[f1] T ≘ T1 → ∀f,T2. ⬆*[f] T ≘ T2 →
                     ∀f2. f2 ⊚ f1 ≘ f → ⬆*[f2] T1 ≘ T2.