The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Hi,
Often I have to prove an equality that can be proven by merely applying transitivity and symmetry on other equalities of the same type in my hypotheses.
I think someone must have already written a tactic which builds an undirected graph of equalities(hypotheses) of the same type and then finds whether a path exists, and build its proof object.
If not, any ideas on the easiest way to achieve this would be appreciated.
Thanks,

-- Abhishek
http://www.cs.cornell.edu/~aa755/