) → (∀n,p,I,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L.ⓑ[I]V1❫ ⊢ T1 ⬆[h,n] T2 →
Q 0 G L V1 V2 → Q n G (L.ⓑ[I]V1) T1 T2 → Q n G L (ⓑ[p,I]V1.T1) (ⓑ[p,I]V2.T2)
) → (∀n,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L❫ ⊢ T1 ⬆[h,n] T2 →
) → (∀n,p,I,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L.ⓑ[I]V1❫ ⊢ T1 ⬆[h,n] T2 →
Q 0 G L V1 V2 → Q n G (L.ⓑ[I]V1) T1 T2 → Q n G L (ⓑ[p,I]V1.T1) (ⓑ[p,I]V2.T2)
) → (∀n,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L❫ ⊢ T1 ⬆[h,n] T2 →