-lemma drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
- ∀K,I,V. L1 = K. 𝕓{I} V →
- (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
- (0 < e ∧ ↓[d, e - 1] K ≡ L2).
+fact drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
+ ∀K,I,V. L1 = K. 𝕓{I} V →
+ (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+ (0 < e ∧ ↓[d, e - 1] K ≡ L2).