Avoid "destruct H" to apply on H itself when H is a section variable.

Need some contorsion for not using the general scheme of naming based
which uses the hypothesis name as base ident, and for instead keeping
a name generated on the type of the section variable, as it was before
for section variables (example of incompatibility in FMapPositive).
Listing a few examples of destruct showing unsatisfactory behaviors.
Enlarge the cases where the like first selection is used in destruct.

This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
More "open" by default for trace debugging.
Reorganization of the test for generic selection of occurrences in
clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.