- λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
- ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2.
+ λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⇧*[f] T1 ≘ U1 →
+ ∀T2. ⇧*[f] T2 ≘ U2 → R T1 T2.
+
+definition liftable2_dx: predicate (relation term) ≝
+ λR. ∀T1,T2. R T1 T2 → ∀f,U2. ⇧*[f] T2 ≘ U2 →
+ ∃∃U1. ⇧*[f] T1 ≘ U1 & R U1 U2.
+
+definition deliftable2_dx: predicate (relation term) ≝
+ λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⇧*[f] T2 ≘ U2 →
+ ∃∃T1. ⇧*[f] T1 ≘ U1 & R T1 T2.