) → (∀n,p,I,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ➡[h] V2 → ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ➡[n,h] 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] V2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
) → (∀n,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ➡[n,h] V2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)
) → (∀n,p,I,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ➡[h] V2 → ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ➡[n,h] 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] V2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
) → (∀n,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ➡[n,h] V2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 →
Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)