elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X;
elim (lift_total V2 0 (i+1)) #U2 #HVU2
lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X;
elim (lift_total V2 0 (i+1)) #U2 #HVU2
lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12