Clarifying the role of ListSet.v in the library, compared to other
finite set libraries.
Fixing detection of occurrences in the presence of nested subterms for
"simpl at" and "change at".
Fixing a little bug with nested but convertible occurrences in "destruct at".
Hopefully the last word on having "simpl f" complying with the
semantics described in the reference manual (i.e. if "f" is a qualid,
do not add implicit arguments and, a fortiori, do not try to solve
these implicit arguments - in particular, changing DbLib which
expected this rule not to be followed).