-definition d_liftable1_all: relation2 lenv term → predicate bool ≝
- λR,b. ∀f,L,K. ⬇*[b, f] L ≡ K →
- ∀Ts,Us. ⬆*[f] 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.