fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
∀L1,L2. TC … (lpx_sn R) L1 L2 →
∀I,K1,V1. L1 = K1.ⓑ{I}V1 →
fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) →
∀L1,L2. TC … (lpx_sn R) L1 L2 →
∀I,K1,V1. L1 = K1.ⓑ{I}V1 →