Make LFSC printer robust to internal types (#8616)

Make LFSC printer robust to internal types (#8616)

This makes the LFSC node converter track the "user declared" symbols and types that it encounters.

It furthermore makes the "dry run" phase of proof printing happen before types and symbols are declared, so that all declared symbols are found before the preamble of LFSC proofs are printed.

These changes are specifically to fix cases where a internal type is generated that does not appear in the input. For example, some preprocessing passes may construct auxiliary uninterpreted sorts.

This fixes 6 more LFSC failures from our regressions.