[1,3: /2 width=4 by fqu_flat_dx, cpxs_flat/
| #H0 destruct /2 width=1 by/
]
-| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
+| #G #L #K #T1 #U1 #m #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (m+1))
#U2 #HTU2 @(ex3_intro … U2)
[1,3: /2 width=10 by cpxs_lift, fqu_drop/
| #H0 destruct /3 width=5 by lift_inj/