#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
[ #L #K #U #T #d #e #HLK #HUT #He #U2 #HU2
elim (lift_total U2 d e) #T2 #HUT2
#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
[ #L #K #U #T #d #e #HLK #HUT #He #U2 #HU2
elim (lift_total U2 d e) #T2 #HUT2