[ -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_sort/
| -HR #i elim (lt_or_ge i (|L1|))
[2: -IH /4 width=4 by lpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux/ ]
[ -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_sort/
| -HR #i elim (lt_or_ge i (|L1|))
[2: -IH /4 width=4 by lpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux/ ]