The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear Lisa Dou,

The problem is that you end your definition with "Qed." This creates a
defintion that is "opaque" and is never unfolded. This make sense for
proofs, but usually not for definitions. If you do not want an opaque
definition use "Defined." instead of "Qed."

All of the proofs that you are looking for can be resolved by using
just one tactic, namely "repeat decide equality". "decide equality" is
a very useful tactic because it solves quite a lot of decision of
equality goals.

Good luck,
Chris Dams