The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Vladimir Voevodsky wrote:
> Is there a way in Coq to make definitions such as:
>
> Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
>
> or
>
> Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 .

Neither of these fits the spirit of inductive definitions.  In each 
example, you might want to assert the final "constructor" as an [Axiom] 
instead, but there is almost always a better way to do such things.  We 
can't comment on the better way(s) for your specific situation without 
more background.