- λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ →
- ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U →
- ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2.
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ →
+ ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U →
+ ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2.