Avoid unwanted subgoals when applying `from_assumption_exact`

Same idea as !342 (closed), but we keep notypeclasses refine, to benefit from the evarconv algorithm. We use shelve explicitly.