elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct -K1
elim (lift_total V2 0 (i+1)) #W2 #HVW2
lapply (tpr_lift … HV12 … HVW1 … HVW2) -V1 /3 width=4/
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct -K1
elim (lift_total V2 0 (i+1)) #W2 #HVW2
lapply (tpr_lift … HV12 … HVW1 … HVW2) -V1 /3 width=4/