#h #g #G #L #T #A #H elim H -G -L -T -A
[ #G #L #k elim (deg_total h g k) /3 width=2 by da_sort, ex_intro/
| * #G #L #K #V #B #i #HLK #_ * /3 width=5 by da_ldef, da_ldec, ex_intro/
#h #g #G #L #T #A #H elim H -G -L -T -A
[ #G #L #k elim (deg_total h g k) /3 width=2 by da_sort, ex_intro/
| * #G #L #K #V #B #i #HLK #_ * /3 width=5 by da_ldef, da_ldec, ex_intro/