#Y #HY #HnY elim HnY -HnY
elim (lpx_inv_unit_sn ā¦ HY) -HY #L2 #HL12 #H destruct
/3 width=3 by lpx_fwd_length, rdeq_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, rdeq_unit_length/