[ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2)
normalize in ⊢ (%→%→?); -I -W1 -W2 -lt /3 width=1 by llpx_sn_skip, ylt_inj/
[ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2)
normalize in ⊢ (%→%→?); -I -W1 -W2 -lt /3 width=1 by llpx_sn_skip, ylt_inj/