-| #f #I #K1 #K2 #_ #IH #L2 #H
- elim (jsx_inv_push_sn … H) -H /3 width=1 by eq_f2/
-| #f #I #K1 #K2 #_ #IH #L2 #H
- elim (jsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
-| #f #I #K1 #K2 #V #_ #_ #IH #L2 #H
- elim (jsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
+| #I #K1 #K #_ #IH #L2 #H
+ elim (jsx_inv_bind_sn … H) -H *
+ [ #K2 #HK2 #H destruct /3 width=1 by jsx_bind/
+ | #J #K2 #V #HK2 #HV #H1 #H2 destruct /3 width=1 by jsx_pair/
+ ]
+| #I #K1 #K #V #_ #HV #IH #L2 #H
+ elim (jsx_inv_void_sn … H) -H #K2 #HK2 #H destruct
+ /3 width=3 by rsx_jsx_trans, jsx_pair/