The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Forgot the list..

On Aug 4, 2012 1:36 PM, "Kristopher Micinski" <krismicinski AT gmail.com> wrote:

Remember, = is notation for eq, and eq_refl is defined inductively only on elements of the same type (those you can demonstrate are convertible), there are alternative encodings of equality you might look into, however (setoids, for example), depending on your needs.

Kris (on a phone)

On Aug 4, 2012 1: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