-lemma length_inv_succ_dx_ltail: ∀L,l. |L| = ⫯l →
- ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K.
-#Y #l #H elim (length_inv_succ_dx … H) -H #I #L #V #Hl #HLK destruct
-elim (lenv_case_tail … L) [2: * #K #J #W ]
-#H destruct /2 width=5 by ex2_3_intro/
+lemma length_inv_succ_dx_ltail: ∀L,n. |L| = ↑n →
+ ∃∃I,K. |K| = n & L = ⓘ{I}.K.
+#Y #n #H elim (length_inv_succ_dx … H) -H #I #L #Hn #HLK destruct
+elim (lenv_case_tail … L) [2: * #K #J ]
+#H destruct /2 width=4 by ex2_2_intro/