#h #L #T #U * -L -T -U
[ #L #k #X #Y #H destruct
| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct
| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct
| #I #L #V #T #U #_ #X #Y #H destruct
| #L #V #T #U #_ #X #Y #H destruct
#h #L #T #U * -L -T -U
[ #L #k #X #Y #H destruct
| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct
| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct
| #I #L #V #T #U #_ #X #Y #H destruct
| #L #V #T #U #_ #X #Y #H destruct