#412 Automatic proof of inequality of datatype constructor with its arguments

[Guillaume Verdier]

Given an inductive datatype, we know that a constructor can't be equal to one of its parameters (e.g., for the classic List datatype, Cons(x, l) ≠ l). This can be proved by induction on l using the injectivity of constructors.
However, some users need this quite often and, when they have datatypes with many inductive constructors, proving it again and again for each constructor becomes tedious.
We could detect this case in the auto rewriter and prove it automatically.