When applied to two terms, aconv returns true if they are
alpha-convertible, and false otherwise. Two terms are alpha-convertible
if they differ only in the way that names have been given to bound variables.
FAILURE
Never fails.
EXAMPLE
- aconv (Term `?x y. x /\ y`) (Term `?y x. y /\ x`)
> val it = true : bool