| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
elim (IHVW2 … HL01) -IHVW2
elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
elim (IHVW2 … HL01) -IHVW2
elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/