- ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ⪤[R, T] K2 →
- ∀b,f. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 →
- ∀U. ⬆*[f] T ≘ U → L1 ⪤[R, U] L2.
+ ∀L1,L2. |L1| = |L2| → ∀K1,K2,T. K1 ⪤[R,T] K2 →
+ ∀b,f. ⬇*[b,f] L1 ≘ K1 → ⬇*[b,f] L2 ≘ K2 →
+ ∀U. ⬆*[f] T ≘ U → L1 ⪤[R,U] L2.