-axiom delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ▶* U2 →
- ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → ∀K. L [dd, ee] ≡ K →
- d ≤ dd → dd + ee ≤ d + e →
- ∃∃T2. K ⊢ T1 [dd - d, e - ee] ▶* T2 & L ⊢ U2 [dd, ee] ≡ T2.
-(*
-#L #U1 #U2 #d #e #H @(tpss_ind_alt … H) -L -U1 -U2 -d -e
-[ #L * #i #d #e #X #dd #ee #H
- [ >(delift_inv_sort1 … H) -X /2 width=3/
- | elim (delift_inv_lref1 … H) -H * [1,3: /3 width=3/ | /3 width=6/ ]
- | >(delift_inv_gref1 … H) -X /2 width=3/
- ]
-| #L #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #T1 #dd #ee #H #K2 #HLK2 #Hdd #Hddee
- lapply
-
- @(ex2_1_intro … X) // /2 width=6/
-*)
+lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdedd
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le … HU1 … HUT1 … HYK ?) -HU1 -HUT1 // -Hdedd #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K → d + e ≤ dd →
+ ∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=3/ qed.
+
+lemma thin_delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K →
+ d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+ ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hdde #Hddee
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le_up … HU1 … HUT1 … HYK ? ? ?) -HU1 -HUT1 // -Hdd -Hdde -Hddee #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K →
+ d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee →
+ ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *)
+
+lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
+ ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hddee
+lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_be … HU1 … HUT1 … HYK ? ?) -HU1 -HUT1 // -Hdd -Hddee #T #HT1 #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
+lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+qed.
+
+lemma thin_delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
+ ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 →
+ ∀K. L [dd, ee] ≡ K → d ≤ dd → dd + ee ≤ d + e →
+ ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
+ L ⊢ U2 [dd, ee] ≡ T2.
+/3 width=3/ qed.