L2 = ⋆.ⓑ{I}V2@@K2.
* #L #K1 #L2 #V1 #T1 #T2 * >append_length #H
elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct
L2 = ⋆.ⓑ{I}V2@@K2.
* #L #K1 #L2 #V1 #T1 #T2 * >append_length #H
elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct