`AC : thm -> term -> thm`

SYNOPSIS
Proves equality of terms using associative, commutative, and optionally idempotence laws.

DESCRIPTION
Suppose _ is a function, which is assumed to be infix in the following syntax, and acth is a theorem expressing associativity and commutativity in the particular canonical form:
```   acth = |- m _ n = n _ m /\
(m _ n) _ p = m _ n _ p /\
m _ n _ p = n _ m _ p
```
Then AC acth will prove equations whose left and right sides can be made identical using these associative and commutative laws. If the input theorem also has idempotence property in this canonical form:
```  |- (p _ q = q _ p) /\
((p _ q) _ r = p _ q _ r) /\
(p _ q _ r = q _ p _ r) /\
(p _ p = p) /\
(p _ p _ q = p _ q)
```
then idempotence will also be applied.

FAILURE CONDITIONS
Fails if the terms are not proved equivalent under the appropriate laws. This may happen because the input theorem does not have the correct canonical form. The latter problem will not in itself cause failure until it is applied to the term.

EXAMPLE
```  # AC ADD_AC `1 + 2 + 3 = 2 + 1 + 3`;;
val it : thm = |- 1 + 2 + 3 = 2 + 1 + 3
# AC CONJ_ACI `p /\ (q /\ p) <=> (p /\ q) /\ (p /\ q)`;;
val it : thm = |- p /\ q /\ p <=> (p /\ q) /\ p /\ q
```