Match with duplicate variables

[BrunoDutertre]

Not sure what's intended but nothing is checking for duplicate variables in a match pattern.
So this is allowed:

(declare sort type)
(declare term type)
(declare cons (! t term (! u term term)))
(declare Bool sort)
(program bad ((t term)) sort (match t ((cons x x) Bool)))

Unfortunately, allowing this can lead to bad results for the same reason as in issue #67:

(declare sort type)
(declare term type)
(declare cons (! t term (! u term term)))
(declare Bool sort)
(declare x type)
(program bad ((t term)) sort (match t ((cons x x) Bool)))
(declare b x)

This fails to check.

[ajreynol]

We should disallow duplicate variables here.