#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
elim (lift_inv_pair_xy_y โฆ HTU)
| #HT
#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
elim (lift_inv_pair_xy_y โฆ HTU)
| #HT