Translate a chain of equivalences A <-> B <-> C into a conjunction
(A <-> B) /\ (B <-> C). Implication is weaker than equivalence when
it occurs to the left of it, and is forbidden at the right hand side.
In other words, A -> B <-> C <-> D is allowed and translated into
A -> ((B <-> C) /\ (C <-> D)), and A <-> B -> C is not allowed,
and requires explicit parentheses.