- λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K →
- ∀T. ⬆*[f] T ≡ U → R K T.
+ λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≘ K →
+ ∀T. ⬆*[f] T ≘ U → R K T.
+
+definition d_deliftable1_isuni: predicate (relation2 lenv term) ≝
+ λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≘ K → 𝐔⦃f⦄ →
+ ∀T. ⬆*[f] T ≘ U → R K T.