The Coq mailing list

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

I've seen the definitional equality of Coq being presented
as a bunch of (mainly computational) rules, e.g. http://adam.chlipala.net/cpdt/html/Equality.html

I've never seen a proof that it is actually a congruence.
Is it just defined as the least congruence containing a bunch
of greek rules? If so, why would such a least relation exist?
(I guess it can be meta-theoretically written as strictly positively inductively defined relation?)

Or, is it completely specified first and then proved to be a congruence? (e.g. in the style of http://www.cs.cornell.edu/Info/Projects/NuPrl/documents/Howe/howeEqualityinLazy_LICS98.ps)

Or something else?

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