- ∀L,T.♯{L, T} < ♯{L0, #i} →
+ ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ →
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
- ∀L,T.♯{L, T} < ♯{L0, #i} →
+ ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ →
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #T #HVT
lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
- ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} →
+ ∀L,T. ⦃L0,ⓑ{a,I}V0.T0⦄ ⊃+ ⦃L,T⦄ →
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
- ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} →
+ ∀L,T. ⦃L0,ⓕ{I}V0.T0⦄ ⊃+ ⦃L,T⦄ →
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
-#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
-[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L #T #IH #L0 * [|*]
+[ #I0 #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
/3 width=10 by cpss_conf_lpss_bind_bind/
elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
/3 width=10 by cpss_conf_lpss_bind_bind/
elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
/3 width=10 by cpss_conf_lpss_flat_flat/
elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
/3 width=10 by cpss_conf_lpss_flat_flat/