+
+(* Basic_1: removed theorems 1: drop1_getl_trans
+*)
+(*
+lemma ldrops_inv_skip2: ∀des2,L1,I,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 →
+ ∀des,i. des ▭ i ≡ des2 →
+ ∃∃K1,V1,des1. des ▭ (i + 1) ≡ des1 &
+ ⇩*[des1] K1 ≡ K2 &
+ ⇧*[des1] V2 ≡ V1 &
+ L1 = K1. 𝕓{I} V1.
+*)
\ No newline at end of file