The Coq mailing list

[Ilya Sergey <ilya.sergey AT imdea.org>]

You can do it by

destruct xyz; destruct p; reflexivity.

in plain Coq, or by 

by case: xyz.

in Coq/SSReflect.

Cheers,

Ilya

On Thu, Aug 14, 2014 at 12:42 PM, Pascal Manoury <pascal.manoury AT pps.univ-paris-diderot.fr> wrote:

Hello,

 don't know how to solve such goal;

  A0 : Set
  B : Set
  C : Set
  xyz : A0 * B * C
  ============================
   (let (p, _) := xyz in let (x, _) := p in x) =
   (let (x, _) := let (x, _) := xyz in x in x)

 Thanks for help,

        Pascal Manoury.