-elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
-elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
-elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2
+elim (ltpr_ltpss_sn_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
+elim (ltpr_ltpss_sn_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
+elim (ltpss_sn_conf … HK1 … HK2) -K #K #HK1 #HK2