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 →