#h #G #L #T1 #A #H elim H -G -L -T1 -A
[ #G #L #s #n /3 width=2 by ex_intro/
| #I #G #K #V1 #B #_ #IH #n -B
cases I -I
[ elim (IH n) -IH #V2 #HV12
#h #G #L #T1 #A #H elim H -G -L -T1 -A
[ #G #L #s #n /3 width=2 by ex_intro/
| #I #G #K #V1 #B #_ #IH #n -B
cases I -I
[ elim (IH n) -IH #V2 #HV12