[ #V5 #T5 #HV5 #HT5 #H destruct
/6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/
| #X #HT1 #H #H0 destruct
[ #V5 #T5 #HV5 #HT5 #H destruct
/6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/
| #X #HT1 #H #H0 destruct