-fact scpes_le_aux: ∀h,g,G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) →
- ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] →
- ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] →
- ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 →
- ∀l21,l22,l. l21 + l ≤ l11 → l22 + l ≤ l12 →
- ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21+l, l22+l] T2.
-#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #l11 #Hl11 #Hl12 #Hl12 #l21 #l22 #l #H1 #H2 * #T0 #HT10 #HT20
-elim (da_inv_sta … Hl11) #X1 #HTX1
-elim (lstas_total … HTX1 (l21+l)) -X1 #X1 #HTX1
-elim (da_inv_sta … Hl12) #X2 #HTX2
-elim (lstas_total … HTX2 (l22+l)) -X2 #X2 #HTX2
-lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hl11 … HTX1 … HT10) -HT10
-[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX1 ]
-lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hl12 … HTX2 … HT20) -HT20
-[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_m_m_commutative #HX2 ]
-lapply (lstas_scpes_trans … Hl11 … HTX1 … HX1) [ // ] -Hl11 -HTX1 -HX1 -H1 #H1
-lapply (lstas_scpes_trans … Hl12 … HTX2 … HX2) [ // ] -Hl12 -HTX2 -HX2 -H2 #H2
-lapply (scpes_canc_dx … H1 … H2) // (**) (* full auto raises NTypeChecker failure *)
+fact scpes_le_aux: ∀h,o,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ ∀G,L,T1. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
+ ∀T2. ⦃G0, L0, T0⦄ >≛[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
+ ∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 →
+ ∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 →
+ ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21+d, d22+d] T2.
+#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #d11 #Hd11 #Hd12 #Hd12 #d21 #d22 #d #H1 #H2 * #T0 #HT10 #HT20
+elim (da_lstas … Hd11 (d21+d)) #X1 #HTX1 #_
+elim (da_lstas … Hd12 (d22+d)) #X2 #HTX2 #_
+lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd11 … HTX1 … HT10) -HT10
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_k_k_commutative #HX1 ]
+lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hd12 … HTX2 … HT20) -HT20
+[1,2,3: // | >eq_minus_O [2: // ] <minus_plus_k_k_commutative #HX2 ]
+lapply (lstas_scpes_trans … Hd11 … HTX1 … HX1) [ // ] -Hd11 -HTX1 -HX1 -H1 #H1
+lapply (lstas_scpes_trans … Hd12 … HTX2 … HX2) [ // ] -Hd12 -HTX2 -HX2 -H2 #H2
+/2 width=4 by scpes_canc_dx/ (**) (* full auto fails *)