Have to refresh the set of universe variables associated to a hint
when it can be used multiple times in a single proof to avoid fixing
a level... A better & less expensive solution should exist.