coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: How to use full induction?

From: Rene Ladan <r.c.ladan AT student.tue.nl>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Re: How to use full induction?
Date: Tue, 19 Oct 2004 20:04:07 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Oct 19, 2004 at 05:51:23PM +0200, Rene Ladan wrote:
> Hi,
>
> I need to use full induction in a proof. Is there a tactic for that
> (not found in the reference manual) or some magic 'Scheme' definition?

After some text book research, it turns out that
"intro m; pattern m; apply lt_wf_ind" is my friend.

Regards,
Rene

[Coq-Club] Re: How to use full induction?, Rene Ladan