[ #_ #X1 #H1 #X2 #H2 -x
>(lpx_sn_inv_atom1 … H1) -X1
>(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/
| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct
elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
[ #_ #X1 #H1 #X2 #H2 -x
>(lpx_sn_inv_atom1 … H1) -X1
>(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/
| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct
elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct