+definition d_liftable1: relation2 lenv term → predicate bool ≝
+ λR,s. ∀K,T. R K T → ∀L,l,m. ⬇[s, l, m] L ≡ K →
+ ∀U. ⬆[l, m] T ≡ U → R L U.
+
+definition d_liftables1: relation2 lenv term → predicate bool ≝
+ λR,s. ∀L,K,cs. ⬇*[s, cs] L ≡ K →
+ ∀T,U. ⬆*[cs] T ≡ U → R K T → R L U.
+
+definition d_liftables1_all: relation2 lenv term → predicate bool ≝
+ λR,s. ∀L,K,cs. ⬇*[s, cs] L ≡ K →
+ ∀Ts,Us. ⬆*[cs] Ts ≡ Us →
+ all … (R K) Ts → all … (R L) Us.
+