(∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
(∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 →
(∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
(∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 →