-lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
- ∀L,U1,d,e. dt + et ≤ d → ↓[d, e] L ≡ K →
- ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 →
- L ⊢ U1 [dt, et] ≫* U2.
-#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -H T2
+lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+ ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
+ ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
+ L ⊢ U1 [dt, et] ▶* U2.
+#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+ elim (lift_total T d e) #U #HTU
+ lapply (IHT … HTU) -IHT #HU1
+ lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
+]
+qed.
+
+lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ▶* T2 →
+ ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
+ ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
+ ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 [dt, et + e] ▶* U2.
+#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2