-elim (IH โฆ HV01 โฆ HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH โฆ HT01 โฆ HT02) -HT01 HT02 IH // #T #HT1 #HT2
-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_eq โฆ HTU1 โฆ HTU2) -HTU1 HTU2 #U #HU1 #HU2
+elim (IH โฆ HV01 โฆ HV02) -HV01 -HV02 // #V #HV1 #HV2
+elim (IH โฆ HT01 โฆ HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
+elim (tpr_tps_bind โฆ HV1 HT1 โฆ HTT1) -T1 #U1 #TTU1 #HTU1
+elim (tpr_tps_bind โฆ HV2 HT2 โฆ HTT2) -T2 #U2 #TTU2 #HTU2
+elim (tps_conf_eq โฆ HTU1 โฆ HTU2) -T #U #HU1 #HU2