The Coq mailing list

["Stefan Monnier" <monnier+lists.coq/news/ AT rum.cs.yale.edu>]

When I try the Discriminate' tactic on something like

     Int=(Exist k t)

it fails because Int and Exist are constructors of a non-small inductive
definition, so it says:

   Error: Incorrect elimination of ee in the inductive type
    Omega
   The elimination predicate Prop has type Type
   It should be one of :
    Prop, Set
   
   Elimination of an inductive object of sort : Set
   is not allowed on a predicate in sort : Type
   because
   strong elimination on non-small inductive types leads to paradoxes.

This happens because the `Discriminate' tactic basically uses a Cases
elimination that either returns False or True.

When I do the proof "manually" I simply use a `Cases' elimination that
returns a boolean and then lift this boolean to Prop, thus avoiding
the strong elimination issue.

Since I have to do that often, I was wondering if someone has already
written a `Discriminate++' that does it for me.


        Stefan