- elim (cpx_lifts … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12 /3 width=1 by drops_refl, drops_drop/
- #U2 #HTU2 #HU12 @(ex3_intro … U2)
- [1,3: /3 width=1 by fqu_drop/
- | #H elim (tdeq_inv_lifts … H … HTU1) -U1
- #X2 #H <(lifts_inj … HTU2 … H) -U2 /2 width=1 by/
- ]
+ elim (cpx_lifts_sn … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12
+ /4 width=6 by fqu_drop, drops_refl, drops_drop, tdeq_inv_lifts_bi, ex3_intro/