X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flifts.ma;h=31f416f12fcec83c6a36b10efd450b9cbf25580c;hb=42705ef31dd3513a998533e02b5f20fb38dd4fb2;hp=d7176d732ac91d30bcfd8d3e1a9a6f654fb02679;hpb=325bc2fb36e8f8db99a152037d71332c9ac7eff9;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 d7176d732..31f416f12 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -15,7 +15,7 @@
 
 include "ground_2/relocation/nstream_after.ma".
 include "basic_2/notation/relations/rliftstar_3.ma".
-include "basic_2/grammar/term.ma".
+include "basic_2/syntax/term.ma".
 
 (* GENERIC RELOCATION FOR TERMS *********************************************)
 
@@ -41,6 +41,21 @@ interpretation "uniform relocation (term)"
 interpretation "generic relocation (term)"
    'RLiftStar f T1 T2 = (lifts f T1 T2).
 
+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 →
+                           ∃∃T2. ⬆*[f] T2 ≡ U2 & R T1 T2.
+
+definition liftable2_bi: predicate (relation term) ≝
+                         λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → 
+                         ∀U2. ⬆*[f] T2 ≡ U2 → R U1 U2.
+
+definition deliftable2_bi: predicate (relation term) ≝
+                           λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 →
+                           ∀T2. ⬆*[f] T2 ≡ U2 → R T1 T2.
 
 (* Basic inversion lemmas ***************************************************)