cc for a setoid?

Stream: general

[Yury G. Kudryashov]

I have a relation with @[refl], @[symm] and @[trans] lemmas. Is there a tactic that closes goals like
r a b → r c b → r a c?

[Kevin Buzzard]

Does cc do it? It stands for congruence closure. You might have to put the statements of refl, symm and trans into your local context.