feat(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT library

This commit adds support for hypotheses (h : C As idxs) where the indices idxs
are just local constants. Before this commit the indices idxs had to be hsets.
Now, they can be hsets or local constants.

The new tests demonstrate new examples that can be handled by the
improved tactic in the HoTT library
feat(frontends/lean): add multiple_instances command

After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command

          multiple_instances <class-name>

closes #370
feat(frontends/lean): add multiple_instances command