Refactor implications + minor additions

[ScriptRaccoon]

• Remove redundant implications¹.
• Group related implications into one².
• Remove "lextensive" property (for now)
• Add proof that Met_c has no sequential colimits.
• Refine Freyd's Lemma: only uses powers, not products.
• Other minor additions

¹Redundant means that they can already be deduced from other implications saved in the database. Most of these cases have been spotted manually. In some cases, though, I have just removed them temporarily and checked with the search feature (which includes a consistency check) if the implication can still be deduced. And in many cases they could, and usually the generated proofs were quite long. This indicates that many more redundant implications are lurking around. I should definitely write a script that detects these (along with redundant property assignments to categories).

²When two implications say A => B and A => C and both are trivial, then just combine them to A => B + C.