- (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
- ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[d + 1, e] T2 → R d e G L V1 V2 →
- R (d+1) e G (L.ⓑ{I}V2) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+ (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] V2 →
+ ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] T2 → R d e G L V1 V2 →
+ R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)