- ∀V,T. ❪G,L❫ ⊢ ⓐV.T ![h,a] → ∀n,X. ❪G,L❫ ⊢ ⓐV.T ➡*[n,h] X →
- ∃∃U. ❪G,L❫ ⊢ T ![h,a] & ❪G,L❫ ⊢ T ➡*[n,h] U & ❪G,L❫ ⊢ ⓐV.U ⬌*[h] X.
+ ∀V,T. ❪G,L❫ ⊢ ⓐV.T ![h,a] → ∀n,X. ❪G,L❫ ⊢ ⓐV.T ➡*[h,n] X →
+ ∃∃U. ❪G,L❫ ⊢ T ![h,a] & ❪G,L❫ ⊢ T ➡*[h,n] U & ❪G,L❫ ⊢ ⓐV.U ⬌*[h] X.