Support arbitrary string types in IPM tactics

The design uses a canonical structure to map types into Coq's string type. As an example, here's a canonical instance for BlueRock's byte strings (bs):

About BS.to_string. (* BS.to_string : bs → string *)
Canonical Structure bsTS : to_str := ToStr BS.to_string.

This now allows us to call iApply "H" even when string_scope is not open or if our bs_scope takes priority over it.

This is trying to work around a missing feature in Coq: tactic notations cannot annotate their arguments with scopes. IPM relies on string_scope being opened and being on top of other string notations. We have about a hundred #[local] Open Scope string_scope in our code base because we rely heavily on byte strings for efficiency in everything that is not IPM. With this MR those can all be removed.

I think the way I engineered this there should not be a trace of the exact string type being used in the final proof term. But I have not checked that super carefully.

As a bonus, here's a performance summary (in billion instructions) for this change on our code base without removing #[local] Open Scope string_scope., i.e. just the overhead of the default to_str instance for string. The fact that the change is negative is a bit confusing and comes from lia caches. What matters is the fact there is no visible regression.

Relative	Master	MR	Change	Files
-0.04%	123983.2	123936.0	-47.2