-definition d_liftable1_all: relation2 lenv term → predicate bool ≝
- λR,s. ∀L,K,t. ⬇*[s, t] L ≡ K →
- ∀Ts,Us. ⬆*[t] Ts ≡ Us →
- all … (R K) Ts → all … (R L) Us.
+definition d_liftable1_all: predicate (relation2 lenv term) ≝
+ λR. ∀K,Ts. all … (R K) Ts →
+ ∀b,f,L. ⬇*[b, f] L ≘ K →
+ ∀Us. ⬆*[f] Ts ≘ Us → all … (R L) Us.