| #a #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
| #a #I #V1 #V2 #T1 #T #T2 #HV12 #_ #HT2 #IHV12 #IHT1 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
elim (IHV12 … HVW1 … HL12) -V1 #W2 #HW12 #HVW2
elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2