Add `add_hypothesis`-like tactic

Coq.Program.Tactics provdes a tactic add_hypothesis, which adds a hypothesis to the context if it does not exist yet. It would be useful to have such a tactic in std++ too, for example, we could use it in the implementation of multiset_solver.

See also the discussion here: !167 (comment 52905)