| #T2 #HT12 #HXT2 #H destruct -IHV
/4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/
]
| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
| #T2 #HT12 #HXT2 #H destruct -IHV
/4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/
]
| #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct