+definition l_liftable1: relation2 lenv term → predicate bool ≝
+ λR,s. ∀K,T. R K T → ∀L,d,e. ⇩[s, d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → R L U.
+
+definition l_liftables1: relation2 lenv term → predicate bool ≝
+ λR,s. ∀L,K,des. ⇩*[s, des] L ≡ K →
+ ∀T,U. ⇧*[des] T ≡ U → R K T → R L U.
+
+definition l_liftables1_all: relation2 lenv term → predicate bool ≝
+ λR,s. ∀L,K,des. ⇩*[s, des] L ≡ K →
+ ∀Ts,Us. ⇧*[des] Ts ≡ Us →
+ all … (R K) Ts → all … (R L) Us.
+