[ /2 width=2 by aaa_sort, ex_intro/
| #I #G #L #K #V #i #HLK #_ * /3 width=6 by aaa_lref, ex_intro/
| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2 by aaa_abbr, aaa_abst, ex_intro/
[ /2 width=2 by aaa_sort, ex_intro/
| #I #G #L #K #V #i #HLK #_ * /3 width=6 by aaa_lref, ex_intro/
| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2 by aaa_abbr, aaa_abst, ex_intro/