-lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 [d, e] ≡ L2 → 0 < d →
- ∃∃K2,V2. K1 [d - 1, e] ≡ K2 &
- K1 ⊢ V1 [d - 1, e] ≡ V2 &
+lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. ▼*[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d →
+ ∃∃K2,V2. ▼*[d - 1, e] K1 ≡ K2 &
+ K1 ⊢ ▼*[d - 1, e] V1 ≡ V2 &