The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

I don't think it is provable since Coq does not support injectivity of
inductive type constructors, which is inconsistent in the presence of
classical axioms.

- Gil

On Sat, Aug 4, 2012 at 7:19 PM, Aleks Nanevski 
<aleks.nanevski AT imdea.org>
 wrote:
> Hi,
>
> Given a nonempty type B, I was wondering if the following is provable:
>
> forall A1 A2 : Type, A1 * B = A2 * B -> A1 = A2
>
> Thanks,
> Aleks