Use variable order in {:inductive} attribute.

[richardlford]

Induction can be applied in two contexts:

• A method, in which case the potential induction variables are all the in-parameters
• A quantifier expression, in which case the potential induction variables are the bound variables
  of the quantifier expression.

The {:inductive} attribute is used to specify that only a subset of the potential
inductive variables be used. The current implementation requires that the given subset
be listed in the same order as they appear in the potential induction variables list.
But there does not seem to be a good reason for this restriction.

We propose that this restriction be removed and that induction be applied in the order
specified in the {:induction} attribute.

[acioc]

Investigation if this is still an issue is for 3.0