(proof-new) Add proof support in TheoryUF (#5002)

(proof-new) Add proof support in TheoryUF (#5002)

This makes TheoryUF use a standard theory inference manager, which thus makes it proof producing when proof-new is enabled.

This additionally cleans HoExtension so that it does not keep a backwards reference to TheoryUF and instead takes its inference manager. This additionally adds two rules for higher-order that are required to make its equality engine proofs correct.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>