elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0
elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0
| #a #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
elim (aaa_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2
lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
| #a #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
elim (aaa_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2
lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0