Display all other properties implied by a property

[danflapjax]

For each property, I would like to be able to see a full list of the properties that it and its converse imply. I'm imagining that it would probably go in a new tab (although it could also go on the Theorems one) with two sections that go, for example, "Metrizable implies:" and "¬Metrizable implies:" each followed by tables of properties in the same style as those for spaces. This can just use the existing deductive engine as well, although we would also probably want to ensure that whenever A ⇒ B is shown that ¬B ⇒ ¬A is also shown.

As a "stretch goal" we would also probably want to distinguish between an implication being unknown versus its existence being disproven by spaces with both A∧B and A∧¬B, but I'm not sure how to represent the latter iconographically in a value column (maybe 🚫 for forbidden?).

This also dovetails with the ideas presented in this discussion, as these derived implications could be used to shortcut other proofs.