X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts.ma;h=afb3e127a6a9b65c02dcd0afe41e0835cb80f1f0;hb=b5ded5b0c305b30349339b24760820154f7de390;hp=73f3be9e7f48bb30597a0689c733e6f73e395eac;hpb=d64caa33426da23e1ab75eca50f227c40e95a24b;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 73f3be9e7..afb3e127a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -41,6 +41,13 @@ 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 deliftable2_sn: predicate (relation term) ≝
+                           λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 →
+                           ∃∃T2. ⬆*[f] T2 ≡ U2 & R T1 T2.
 
 (* Basic inversion lemmas ***************************************************)