∃∃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 ]
∃∃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 ]