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