coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] equation (eq) and irrefutable patterns (let .. in ..)

From: Pascal Manoury <pascal.manoury AT pps.univ-paris-diderot.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] equation (eq) and irrefutable patterns (let .. in ..)
Date: Thu, 14 Aug 2014 12:42:52 +0200

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.

[Coq-Club] equation (eq) and irrefutable patterns (let .. in ..), Pascal Manoury, 08/14/2014
- Re: [Coq-Club] equation (eq) and irrefutable patterns (let .. in ..), Ilya Sergey, 08/14/2014