The Coq mailing list

["Conor McBride" <ctm AT dcs.ed.ac.uk>]

h>    Inductive jmeq : (A:Type)(B:Type) A -> B -> Prop :=
h>      jmrefl : (A:Type)(a:A)(jmeq A A a a).

But that `Inductive' is a little misleading, because the elimination
rule is

majorJ : (A:Type)(a:A)(Phi:(a':A)(q:jmeq a a')Type)
           (Phi a (jmrefl a))->
            Phi a' q

That isn't what you get from an `Inductive' definition. The standard
`Inductive' elim rule for jmeq is totally useless.

majorJ, on the other hand, is a lot more useful than any number of
Conservative Prime Ministers.

Of course, this majorJ isn't conservative at all...

Conor

PS Could somebody please add me to this mailing list? I get very lonely
   these days. All 
lego-club AT dcs.ed.ac.uk
 ever gets is confused people
   complaining that there's a piece missing from the kit they bought
   their 9-year-old.