elim (IHU12 … HTU1) -IHU12 -HTU1
/3 width=6 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
elim (IHU12 … HTU1) -IHU12 -HTU1
/3 width=6 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd