| #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1
lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2; normalize /2/ -Hde2i1 #HWT2
| #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1
lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2; normalize /2/ -Hde2i1 #HWT2