-fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 [d, e1] ▶ T2 → ∀e2. e1 = e2 + 1 →
- ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e2] ▶ T2.
+fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 ▶ [d, e1] T2 → ∀e2. e1 = e2 + 1 →
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶ [d + 1, e2] T2.