elim (append_inj_dx … H ?) -H // -HX #_ #H destruct -X
lapply (ltpss_sn_fwd_length … HL2) >append_length >append_length #H
lapply (injective_plus_r … H) -H #H
elim (append_inj_dx … H ?) -H // -HX #_ #H destruct -X
lapply (ltpss_sn_fwd_length … HL2) >append_length >append_length #H
lapply (injective_plus_r … H) -H #H