The Coq mailing list

[David Monniaux <David.Monniaux AT ens.fr>]

I have the following definition:

 Inductive comp_widening_chain (S : Set) : Set :=
   comp_widening_chain_intro : forall x : S,
     (forall y : S,
       (option (comp_widening_chain S))) -> (comp_widening_chain S).

If I try to do reasonings by induction using the "induction" or "elim" 
on such a datatype, I don't get an induction hypothesis.

I'm forced to use

refine (fix inductive_predicate (foobar : comp_widening_chain) : ... := _)

But that's clunky, and, I'm afraid, this seems to lead to weird error 
messages (see other mail).

What is the correct way of doing induction on such things?

Regards,
DM