∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2.
#L1 #L2 #n1 #n2 #H #HL12
lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0
∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2.
#L1 #L2 #n1 #n2 #H #HL12
lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0