Move `yes and `no to Reflection.Syntax

[WhatisRT]

These are generally useful for writing things involving Dec, so they should live in a more accessible place.

[omelkonian]

I don't think that's the way to go with these things, due to the Fairbairn threshold: we cannot provide quoted version of every possible term in stdlib, hence why we define shorthands locally only when we need them (e.g. yes/no when deriving DecEq).

If it happens that multiple tactics work on, say, decidability proofs, it would make sense to keep a common score file just for this subset of tactics (e.g. living under Tactics.Dec.Core).

[WhatisRT]

I generally agree, but I think in this case it's an exception because it has so many potential use cases. Other examples I can think of are quoted equality and a quoted case_of_. These are just too useful not to share.

I do think that maybe this module is not the best place, but this library should get a proper reorganization anyway and I didn't want to spend too much time thinking about it right now.

[omelkonian]

But shouldn't we follow a more pull-based/on-demand approach, only introducing shorthands that have at least more than 1 use?

[WhatisRT]

You're right. In this case there are downstream use cases. They currently aren't relevant, but if something was useful in the past I think it's a good indication that it would be useful in the future.

I'll be a bit less lazy and add a few things & move them to a better location.