Add, document, and enforce the policy that <cond> variables should

only have one definition.

Having this policy simplifies the AST rewriter code. The policy is
enforced through verification. This commit also re-structures most of
the verifier code from a class to a collection of functions.