-elim (tpr_pts_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
-elim (tpr_pts_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
-elim (pts_conf … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
+elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
+elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
+elim (tps_conf … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2