T906: Urysohn's metrization theorem

[prabau]

Adding the Urysohn's metrization theorem:

• second countable + T3 => metrizable.

Previously, it was derivable from some non-trivial results about $\aleph$-spaces. Since it's such an important result, it seems worth to have it explicitly.

[prabau]

For some reason
π-Base, Search for Second countable + T3 + ~Metrizable
still derives this using $\aleph$-spaces instead of the new theorem.

@yhx-12243 you may have some idea. A limitation of the derivation engine?

[prabau]

It seems that the reason for ignoring the new result is that the new uid T906 is too large. So the engine finds some (non-optimal) derivation using various smaller uids and always ignores the new one. I am guessing the engine tries smaller uids first.
I'll move the new one.

@yhx-12243 fyi

[yhx-12243]

My plan is to fully rewrite the engine that using cadical or Z3, which will resolve pi-base/web#199. However, it's still in progress and maybe conflict with pi-base/web#235.

These professional solvers can create some derive graph that is smaller on effort. The only issue is maybe it can be slower a bit (but I think for such structured clauses in pi-base it won't sacrifice many efficiency).