elim (rsx_inv_flat … HL) -HL #HV1 #HL
elim (rsx_inv_bind_void … HL) -HL #HW1 #HT1
/6 width=8 by jsx_pair, rsx_lifts, rsx_bind_void, rsx_flat, drops_refl, drops_drop/
elim (rsx_inv_flat … HL) -HL #HV1 #HL
elim (rsx_inv_bind_void … HL) -HL #HW1 #HT1
/6 width=8 by jsx_pair, rsx_lifts, rsx_bind_void, rsx_flat, drops_refl, drops_drop/