elim (tpr_inv_abbr1 … H) -H *
[ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
lapply (IH … HA … (L2.ⓓV2) … HT1) -IH -HA -HT1 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
elim (tpr_inv_abbr1 … H) -H *
[ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2
lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
lapply (IH … HA … (L2.ⓓV2) … HT1) -IH -HA -HT1 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/