The Coq mailing list

[David Baelde <david.baelde AT gmail.com>]

Hi Jeffrey,

Sometimes it's obvious that two things are equal, you just have to
compute and look, for example in x = x or 1+1 = 2. Sometimes it takes
a (more or less) complex argument. For example, 1+x = x+1 holds but it
takes more than computing a sum to check it -- you have to prove it by
induction on the natural number x. The boundary between trivial and
non-trivial varies from one human to another, and from one system to
another.

In your code Coq, it is not obvious that x and x0 have the same type.
This is because of a limitation in the typing of pattern matching. It
requires you to write a proof by hand or, as Dimitri pointed out,
rewrite the definition in a way that makes things obvious for Coq.

Hope this helps,
-- 
David