| #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct
elim (IHLK1 … HK12) #K #HL1K #HK2
lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
| #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct
elim (IHLK1 … HK12) #K #HL1K #HK2
lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA