Better formalization of regular expression unfolding skolems (#6602)

Better formalization of regular expression unfolding skolems (#6602)

This replaces our previous formalization of RE unfolding skolems with a more explicit one that is amenable to external proof conversion. It adds a few associated utility methods to SkolemManager required for LFSC proof conversion for RE_UNFOLD_POS.

It also changes the order of equalities in the RE_UNFOLD_POS rule, which simplifies LFSC proof checking.