-lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,s,d,e. ⬇[s, d, e] L2 ≡ L1 →
- ∀T1. ⬆[d, e] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
+lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,s,l,m. ⬇[s, l, m] L2 ≡ L1 →
+ ∀T1. ⬆[l, m] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.