Use name arg for `solve_can_be_split_for` to avoid universe issues

[tahina-pro]

The automatic introduction of exists_ and pure mechanism in Steel relies on the Steel tactic identifying lemmas by their attributes:

1. It finds all lemmas tagged solve_can_be_split_lookup.
2. Among them, it finds all lemmas tagged solve_can_be_split_for exists_

In the latter step, @W95Psp raised an issue: exists_ is universe-polymorphic. Thus, the attribute is universe-polymorphic as well. So, @nikswamy proposed to replace the argument to solve_can_be_split_for by a string representing the name of the head symbol of the vprop to solve for automatic introduction, replacing the attribute with:

solve_can_be_split_for (`%exists_)

This PR is exactly implementing that solution (and similarly for solve_can_be_split_forall_dep_for.)

I have an Everest green: project-everest/everest@1fe3844285c1973cd4edc9490f417292f3ebec5e