Improve "decompose_Forall_hyps" tactic.
Improve "choosing an element" of a finite collection.