X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts.ma;h=31f416f12fcec83c6a36b10efd450b9cbf25580c;hb=268e7f336d036f77ffc9663358e9afda92b97730;hp=6f0cef9d0be252cf2e58847e28a0d538b1b36101;hpb=2f00c2224c66757d00883602cfd0bbd2448eb3ca;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
index 6f0cef9d0..31f416f12 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -41,9 +41,9 @@ interpretation "uniform relocation (term)"
 interpretation "generic relocation (term)"
    'RLiftStar f T1 T2 = (lifts f T1 T2).
 
-definition liftable2: predicate (relation term) ≝
-                      λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → 
-                      ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2.
+definition liftable2_sn: predicate (relation term) ≝
+                         λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → 
+                         ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2.
 
 definition deliftable2_sn: predicate (relation term) ≝
                            λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 →