| #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_appl … H) -H #B2 #_ #HA2
lapply (IHA1 … HA2) -L #H destruct //
| #G #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
| #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_appl … H) -H #B2 #_ #HA2
lapply (IHA1 … HA2) -L #H destruct //
| #G #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H