X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts.ma;h=681363f03ff4c25db723b563f6000441ae5f190c;hp=060f3b8057d843e509201ed69a526d62895c6f01;hb=31be09cc0d040577917783e050e1d38c0daa8f01;hpb=bf2b1df641df98a3b614a8c3d53edee8beb0964a

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index 060f3b805..681363f03 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -56,6 +56,10 @@ definition deliftable2_bi: predicate (relation term) ≝
                            λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
                            ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2.
 
+definition liftable2_dx: predicate (relation term) ≝
+                         λR. ∀T1,T2. R T1 T2 → ∀f,U2. ⬆*[f] T2 ≘ U2 →
+                         ∃∃U1. ⬆*[f] T1 ≘ U1 & R U1 U2.
+
 definition deliftable2_dx: predicate (relation term) ≝
                            λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 →
                            ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2.
@@ -333,6 +337,11 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma liftable2_sn_dx (R): symmetric … R → liftable2_sn R → liftable2_dx R.
+#R #H2R #H1R #T1 #T2 #HT12 #f #U2 #HTU2
+elim (H1R … T1 … HTU2) -H1R /3 width=3 by ex2_intro/
+qed-.
+
 lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R.
 #R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2
 elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/
@@ -365,7 +374,7 @@ elim (IHV1 f) -IHV1 #V2 #HV12
 ]
 qed-.
 
-lemma lifts_push_zero (f): ⬆*[⫯f]#O ≘ #0.
+lemma lifts_push_zero (f): ⬆*[⫯f]#0 ≘ #0.
 /2 width=1 by lifts_lref/ qed.
 
 lemma lifts_push_lref (f) (i1) (i2): ⬆*[f]#i1 ≘ #i2 → ⬆*[⫯f]#(↑i1) ≘ #(↑i2).