#Y #HY #HnY elim HnY -HnY
elim (lpx_inv_unit_sn … HY) -HY #L2 #HL12 #H destruct
/3 width=3 by lpx_fwd_length, reqx_unit_length/
#Y #HY #HnY elim HnY -HnY
elim (lpx_inv_unit_sn … HY) -HY #L2 #HL12 #H destruct
/3 width=3 by lpx_fwd_length, reqx_unit_length/