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