The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> Structurally equal types are equal.  What you mean is "two inductive types
> that have the same constructors with the same argument types",

Nitpick: isn't this more or less the "definition" of "structurally equal"?
More to the point, if you take the "paper" definition of inductive types
with calculus like

    e ::= ... | Ind(x : e, \vec e) | Con(e, n) | Case(...)
    
then I believe you'd get that "two inductive types that have the same
constructors with the same argument types" would indeed be equal.

IOW the reason they're not equal is because Coq uses a kind of "name
equality" or "generativity" of inductive definitions.

[ The above may look like a statement, but it's really a question in
  disguise, because I'm not really sure this is handled by Coq.  ]
  

        Stefan