| llpx_sn_sort: ∀L1,L2,d,k. |L1| = |L2| → llpx_sn R d (⋆k) L1 L2
| llpx_sn_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn R d (#i) L1 L2
| llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
| llpx_sn_sort: ∀L1,L2,d,k. |L1| = |L2| → llpx_sn R d (⋆k) L1 L2
| llpx_sn_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn R d (#i) L1 L2
| llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →