severe bug found in parallel zeta

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / lifts_lifts.ma

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 41c641716a280339f1c67ae399d534dead1e23aa..0581f6d1c3a28dc4b3b07b25473737a83e54a537 100644 (file)
--- 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.