lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct
>(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/
lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct
>(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/