-| /3 width=2 by cpx_cpxs, cpx_ess/
-| #I #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H
- elim (lpx_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct
- /4 width=3 by cpxs_delta, cpxs_strap2/
-| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H
- elim (lpx_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct
- /4 width=3 by cpxs_lref, cpxs_strap2/
-|5,10: /4 width=1 by cpxs_beta, cpxs_bind, lpx_bind_refl_dx/
-|6,8,9: /3 width=1 by cpxs_flat, cpxs_ee, cpxs_eps/
-| /4 width=3 by cpxs_zeta, lpx_bind_refl_dx/
-| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_bind_refl_dx/
+| /3 width=2 by cpm_cpms/
+| #n #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H
+ elim (lpr_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct
+ /4 width=3 by cpms_delta, cpms_step_sn/
+| #n #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H
+ elim (lpr_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct
+ /4 width=3 by cpms_ell, cpms_step_sn/
+| #n #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H
+ elim (lpr_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct
+ /4 width=3 by cpms_lref, cpms_step_sn/
+| /4 width=1 by cpms_bind, lpr_bind_refl_dx/
+| /3 width=1 by cpms_appl/
+| /3 width=1 by cpms_cast/
+| /4 width=3 by cpms_zeta, lpr_bind_refl_dx/
+| /3 width=1 by cpms_eps/
+| /3 width=1 by cpms_ee/
+| /4 width=1 by lpr_bind_refl_dx, cpms_beta/
+| /4 width=3 by lpr_bind_refl_dx, cpms_theta/