coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

[Coq-Club] reasoning out of type equalities, Aleks Nanevski, 08/04/2012
- Message not available
  - Re: [Coq-Club] reasoning out of type equalities, Kristopher Micinski, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Chung-Kil Hur, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/04/2012
  - Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
  - Re: [Coq-Club] reasoning out of type equalities, andré hirschowitz, 08/05/2012
    - Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
      - Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
        
        Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
        
        Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
        
        Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012