X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops.ma;h=7a4ad7662881ea68e23f3f77f8e7062914e763fa;hb=38571b4c3881f2b59b7a2cdd016c83b161d3d755;hp=d35fb52a2b748ca31c6c7d8542c5bd241e5b0f0d;hpb=6bfdcdaf50cc3e5ca25079cd4006aeefac73c8c2;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index d35fb52a2..7a4ad7662 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -42,6 +42,10 @@ definition d_liftable1: predicate (relation2 lenv term) ≝
                         λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K →
                         ∀U. ⬆*[f] T ≡ U → R L U.
 
+definition d_deliftable1: predicate (relation2 lenv term) ≝
+                          λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K →
+                          ∀T. ⬆*[f] T ≡ U → R K T.
+
 definition d_liftable2: predicate (lenv → relation term) ≝
                         λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
                         ∀U1. ⬆*[f] T1 ≡ U1 →