lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
/4 width=7 by cpx_delta, cpr_cpx, lstas_cpr/
| /4 width=2 by cpx_bind, da_inv_bind/
lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
/4 width=7 by cpx_delta, cpr_cpx, lstas_cpr/
| /4 width=2 by cpx_bind, da_inv_bind/