- lapply (drop_conf_ge … H … HLK2 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK20
- elim (IHx K10 W10 … K20 0) -IHx -HL12 /3 width=6 by drop_fwd_rfw/
- elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 //
+ lapply (drop_conf_ge … H … HLK2 ?) -H /2 width=1 by ylt_fwd_le_succ1/ <minus_plus #HK20
+ elim (IHx K10 W10 … K20 0 ?) -IHx -HL12 /3 width=6 by drop_fwd_rfw/
+ elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 /2 width=6 by/