-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.
+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.