#h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
[ elim (deg_total h o s1) #d1 #H1
elim (deg_total h o s2) #d2 #H2
#h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
[ elim (deg_total h o s1) #d1 #H1
elim (deg_total h o s2) #d2 #H2