elim (lift_trans_le … HUV … HVW ?) -HUV HVW V // >arith_a2 // -Hid /3/
| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X;
elim (lift_trans_le … HUV … HVW ?) -HUV HVW V // >arith_a2 // -Hid /3/
| #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct -X;