The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 5 Sep 2007, Marko Malikovi? wrote:

> Thank you also,
>
> but I need just to inductive "build up" subgoals like this:
>
> Coq <
> Coq < Goal forall x:nat, in_subset x -> x<6.
> 1 subgoal
>
>  ============================
>   forall x : nat, in_subset x -> x < 6
>
> Unnamed_thm < intros x H;induction H.
> 5 subgoals
>
> With "normally" definition I obtain subgoals which need more required
> tactics.

I understand.  What I am suggesting you do is

intros x H; induction H using in_subset_ind'.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''