-[ #I #L #J #W1 #U1 #H destruct
-| #L #k #l #_ #J #W1 #U1 #H destruct
-| #I #L #K #V #V2 #W2 #i #_ #_ #_ #J #W1 #U1 #H destruct
-| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #W1 #U1 #H destruct
-| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=5/
-| #L #V #T1 #T #T2 #_ #_ #J #W1 #U1 #H destruct
-| #L #V #T1 #T2 #HT12 #J #W1 #U1 #H destruct /3 width=1/
-| #L #V1 #V2 #T #HV12 #J #W1 #U1 #H destruct /3 width=1/
-| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=11/
-| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=13/
+[ #I #L #J #W #U1 #H destruct
+| #L #k #l #_ #J #W #U1 #H destruct
+| #I #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
+| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=5/
+| #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct
+| #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=1/
+| #L #V1 #V2 #T #HV12 #J #W #U1 #H destruct /3 width=1/
+| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11/
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13/