How does cc work?

Stream: general

[Bryan Gin-ge Chen]

Following a suggestion of @Joseph Myers in #6469, I've been playing around with refactoring boolean_algebra so that it extends a "generalized boolean algebra" class (basically, Boolean algebras which may not have \top, e.g. finset a for a not necessarily fintype) in branch#symm_diff_generalized_boolean_algebra.

However, some proofs by cc have been breaking, e.g. finset.filter_ne and sym2.is_diag_iff_proj_eq. So far I've been able to fix them, but I want to make sure I haven't made some poor decision with the way that I'm structuring the classes. Does cc rely on certain definitional equalities to work or is there something else that I changed that's the culprit?