- ∨∨ ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ U0 ➡ T2 &
- U2 = ⓐV2. T2
- | ∃∃V2,W,T1,T2. L ⊢ V1 ➡ V2 & L. ⓓV2 ⊢ T1 ➡ T2 &
- U0 = ⓛW. T1 &
- U2 = ⓓV2. T2
- | ∃∃V2,V,W1,W2,T1,T2. L ⊢ V1 ➡ V2 & L ⊢ W1 ➡ W2 & L. ⓓW2 ⊢ T1 ➡ T2 &
- ⇧[0,1] V2 ≡ V &
- U0 = ⓓW1. T1 &
- U2 = ⓓW2. ⓐV. T2.
+ ∨∨ ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ U0 ➡ T2 &
+ U2 = ⓐV2. T2
+ | ∃∃a,V2,W,T1,T2. L ⊢ V1 ➡ V2 & L. ⓓV2 ⊢ T1 ➡ T2 &
+ U0 = ⓛ{a}W. T1 &
+ U2 = ⓓ{a}V2. T2
+ | ∃∃a,V2,V,W1,W2,T1,T2. L ⊢ V1 ➡ V2 & L ⊢ W1 ➡ W2 & L. ⓓW2 ⊢ T1 ➡ T2 &
+ ⇧[0,1] V2 ≡ V &
+ U0 = ⓓ{a}W1. T1 &
+ U2 = ⓓ{a}W2. ⓐV. T2.