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 ***************************************************)