Confluent relations

This MR adds:

• The symmetric and reflexive/transitive/symmetric closure of a relation
• Different notions of confluence: diamond property, confluence, local confluence (following the naming conventions in https://www21.in.tum.de/~nipkow/TRaAT/)
• Standard properties such as diamond ⊢ confluence ⊢ local confluence, the Church-Rosser property, Newman's lemma

As part of this MR, I removed the hint database ars. The name made no sense and it was not used anywhere to my knowledge. If it was used anywhere, it would be very unreliable as it contained hints like rtc_trans that would generally lead to loops.

added 3 commits

• 7120347d - Remove `ars` hint database.
• 0e3fa79b - The symmetric and reflexive/transitive/symmetric closure.
• 01c0b6b1 - The different notions of confluence and properties about them.

Compare with previous version

Looks good, can you merge this?

Other than the nit, LGTM!

added 8 commits

• 01c0b6b1...a99446f9 - 5 commits from branch master
• 51d69170 - Remove `ars` hint database.
• c73f285d - The symmetric and reflexive/transitive/symmetric closure.
• 89454051 - The different notions of confluence and properties about them.

Compare with previous version

resolved all discussions

Merging, thanks!

mentioned in commit 87b2fe62

merged