Define more HFS constants; prove lemmas about them

Inspired by ITP talk on paper "Hereditarily Finite Sets in Constructive
Type Theory" by Smolka and Stark.

Rename: qcase_tac/rename1; Q.FIND_CASE_TAC/Q.RENAME1_TAC

This use of the "case" substring was just confusing given things like
Cases_on. The "1" is there because I want to now implement a more
general version that
- deals with the issue (identified in the .doc file), where existing
names in the goal can still get in the way; and
- allows multiple subterms to be matched and renamed as a unit

Though seemingly independent, the second feature is really needed if the
first is to be done: implementing the first will require all the free
variables in a goal to be renamed away (to genvars, I expect), and then
it's impossible to ground particular matches against known free
variables.

Not "hierarchically" finite; "hereditarily" finite

Example: define type of hierarchically finite sets