| #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_abbr … H) -H /2 width=1/
| #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
| #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_abbr … H) -H /2 width=1/
| #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H