#h #a #G #K #W #HW #U #HWU
lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU)
/3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/
#h #a #G #K #W #HW #U #HWU
lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU)
/3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/