lapply (cpy_weak … H 0 (d+e) ? ?) -H // #H
elim (cpy_inv_lift1_be … H … H0LK … HVW2) -H -H0LK -HVW2
/3 width=7 by cpysa_subst, ylt_fwd_le_succ/
lapply (cpy_weak … H 0 (d+e) ? ?) -H // #H
elim (cpy_inv_lift1_be … H … H0LK … HVW2) -H -H0LK -HVW2
/3 width=7 by cpysa_subst, ylt_fwd_le_succ/