elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
/4 width=6 by cprs_strap2, cprs_delta/
|3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/
elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
/4 width=6 by cprs_strap2, cprs_delta/
|3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/