-| #L2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
- elim (lift_inv_flat2 … H) -H #U1 #T1 #HU12 #HT12 #H destruct
- elim (IHTU2 … HL21 … HT12) -L2 -HT12 #U0 #HTU0 #HU02
- lapply (lift_inj … HU02 … HU12) -HU02 #H destruct /3 width=3/
+| #L2 #W2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+ elim (lift_inv_flat2 … H) -H #W1 #T1 #_ #HT12 #H destruct
+ elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=3/