elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
/4 width=7 by cpxs_delta, cpxs_strap2/
|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/
elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
/4 width=7 by cpxs_delta, cpxs_strap2/
|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/