- ⋆. ⓑ{I1} V1 ⊢ T1 [O, 1] ▶ TT1 →
- ⋆. ⓑ{I1} V2 ⊢ T2 [O, 1] ▶ TT2 →
+ ⋆. ⓑ{I1} V1 ⊢ T1 ▶ [O, 1] TT1 →
+ ⋆. ⓑ{I1} V2 ⊢ T2 ▶ [O, 1] TT2 →
∃∃X. ⓑ{I1} V1. TT1 ➡ X & ⓑ{I1} V2. TT2 ➡ X.
#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
∃∃X. ⓑ{I1} V1. TT1 ➡ X & ⓑ{I1} V2. TT2 ➡ X.
#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 →
∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X.
#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 →
∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X.
#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20