Remove singular case from `distinct_elim`
SMT-LIB doesn't allow distinct to be applied to only one argument. veriT and other solvers, however accept it.
In this context the rule distinct t = ⊤ is sensible.
However, it leads to confusion, and makes Alethe harder to support in some restrictive systems (like Eunoia).
Hence, this case should be removed from the reference. Solvers are free to generate proofs using it for non-standard SMT-LIB benchmarks.