The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Edward Z. Yang wrote:
>      n : nat
>      a : A
>      b : B n
>      f : P (a * b)
>      -------------
>      ... (a, b) ...
>
> then induction on f will fail with "b is used in hypothesis", whereas
>
>      n : nat
>      ab : A * B n
>      f : P ab
>      -------------
>      ... ab ...
>
> Will work fine.  What's the correct tactic to interconvert? 'set' doesn't 
> quite
> seem to do the right thing.
>    

Often the cleanest approach is to prove a lemma, which will have a 
single variable standing for the pair.  You can also use [generalize 
dependent] in some cases.

(I assume [P (a * b)] above should be [P (a, b)].)