[ #G #L #s #A2 #H >(aaa_inv_sort … H) -H //
| #I1 #G #L #V1 #B #_ #IH #A2 #H
elim (aaa_inv_zero … H) -H #I2 #K2 #V2 #H #HA2 destruct /2 width=1 by/
[ #G #L #s #A2 #H >(aaa_inv_sort … H) -H //
| #I1 #G #L #V1 #B #_ #IH #A2 #H
elim (aaa_inv_zero … H) -H #I2 #K2 #V2 #H #HA2 destruct /2 width=1 by/