#G #L #I #K #V #i #HLK #H
elim (lifts_total V (šāØāiā©)) #W #HVW
lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
#G #L #I #K #V #i #HLK #H
elim (lifts_total V (šāØāiā©)) #W #HVW
lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK