#HiL #l elim (ylt_split i l) /2 width=1 by llpx_sn_skip/
elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
qed-.
lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
#HiL #l elim (ylt_split i l) /2 width=1 by llpx_sn_skip/
elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
qed-.
lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T