Fix bug in handling of distinctness for large enumerated types

Previous attempt at regression test for this didn't capture scenario
where srw_ss() had already been initialised and correctness relied on
TypeBase hook telling BasicProvers about newly arriving tyinfo.

Performance is still bad when theories dump large tyinfos to disk.