+ lapply (rpx_inv_lifts_bi … H1 (Ⓣ) … HTU0) -H1 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #H1
+ lapply (rdeq_inv_lifts_bi … H2 (Ⓣ) … HTU0) -H2 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #H2
+ elim (tdeq_inv_lifts_sn … HU02 … HTU0) -U0 #T2 #HTU2 #HT02