congruence closure for uninterpreted functions aware decision procedures

[ordinarymath]

Lean has recently officially announced grind. It would be good to have a similar tactic. A good start should probably be just porting over old HOL work by boulton https://link.springer.com/chapter/10.1007/3-540-60275-5_58