- lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 (**) (* auto too slow without trace *)
- @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
+ lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=2 by ldrop_drop/ #HV24
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5
+ @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/