The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Mon, Jul 15, 2013 at 3:19 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

> Generally this work is easy to push off onto [congruence], which is a
> complete decision procedure for equality with constructors.

Hm.. Not complete enough, it seems. I oversimplified my original example.
How would you prove the following?

Inductive Structure :=
  |  shapeA:  Structure' -> Structure
  |  shapeB:                Structure
with Structure' :=
  |  shapeA': Structure  -> Structure'
  |  shapeB':               Structure'.

Goal forall x, (shapeA (shapeA' x)) <> x.
  intro.
  congruence. (* Error: congruence failed *)

--
www.mhelvens.net