elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X;
lapply (tps_fwd_tw … HV01) #H2
lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H
elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X;
lapply (tps_fwd_tw … HV01) #H2
lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H