#L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm
elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct
elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct
#L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm
elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct
elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct