Introduce an attribute to unrefine type arguments

[mtzguido]

This PR allows to tag certain type implicits with the @@@unrefine attribute, causing the unifier to attempt to peel away all refinements of the type before instantiating the uvar. With this, if x is nat, the equality x == x will happen at type int instead of nat as currently happens. This can be desirable if we try to relate this fact to, say, 0 == 0, which defaults to int as 0 is an int literal.

This is potentially controversial and can break some code, see also the do_not_unrefine attribute to fix some regressions. Hence, this logic is only enabled if --debug __unrefine is passed (I will turn this into an extension flag --ext, but the extension mechanism is currently inefficient and I don't want to slow down F*).