The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Thu, Oct 31, 2002 at 06:45:35PM +0100, Pierre Courtieu wrote:

> In this case, you just need to reduce, for example with the Simpl
> tactic (see below).

> In the case where the decreasing argument does not start with a
> constructor (see how' below), then the only way I know is to proceed
> by case.

Thanks, indeed in my "real" lemma, I haven't a constructor
up-front. Case didn't do the job either, because of the specifics of
the actual "P" I had, itself a fixpoint. But generalising into a
theorem similar to the "How" of my message, proving it with the "Case"
and applying it where I had the problem worked great.

-- 
Lionel

Attachment: pgpg6XseS9ejG.pgp
Description: PGP signature