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 liftable2_sn: predicate (relation term) ≝
λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⇧*[f] T1 ≘ U1 →
∃∃U2. ⇧*[f] T2 ≘ U2 & R U1 U2.