2 Basic Constructs

VAR-DECL can appear both as a BASIC-ITEM and inside a QUANTIFICATION. What is allowed concerning re-use of variables and is the treatment the same in both contexts?

What is said in version 0.95 of the language description seems inconsistent:

Section 2, before 2.1: "it is not allowed to specify the same BASIC-ITEM more than once in the same list BASIC-ITEM*."
Section 2.2 (VAR-DECL): "The variables in the list VAR+ must be ... distinct from the variables previously declared by other VAR-DECLs in the same list of basic items"
Section 2.3.1 (QUANTIFICATION): "an inner declaration for a variable with the same identifier as in an outer declaration overrides the outer declaration"

The treatment of VAR-DECL in QUANTIFICATION need not be the same as its treatment in BASIC-ITEM, although there should be a good reason if a non-uniform treatment is chosen.

A related question concerns repetition, i.e. redeclaration of a variable with the same sort as before:

var x:s  ...  ...  var x:s

var x:s  ...  ...  axiom forall x:s. phi

axiom forall x:s. (... forall x:s. phi ...)