The Coq mailing list

["Edward Z. Yang" <ezyang AT mit.edu>]

What is the difference between:

    a : A
    b : B
    ----------
    ... (a, b) ...

and

    ab : A * B
    ----------
    ... ab ....

?

I would think that there is no difference, but in fact if A and B are
dependent you might have this situation:

    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.

Edward