coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Hi,

Given (x y : Prop), I’m wondering about how to coerce an equality proof for (@eq Type x y) to (@eq Prop x y).

Is this possible?

Thanks,

Leo

[Coq-Club] coercing equality proofs, Leonardo de Moura, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
  - Re: [Coq-Club] coercing equality proofs, Vladimir Voevodsky, 01/28/2014
    - Re: [Coq-Club] coercing equality proofs, Jeremy Avigad, 01/28/2014
      - Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
        
        Re: [Coq-Club] coercing equality proofs, Cody Roux, 01/28/2014
        
        Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
        
        Re: [Coq-Club] coercing equality proofs, Cody Roux, 01/28/2014
      - Re: [Coq-Club] coercing equality proofs, Vladimir Voevodsky, 01/28/2014
        
        Re: [Coq-Club] coercing equality proofs, Bas Spitters, 01/29/2014
        
        Re: [Coq-Club] coercing equality proofs, Arnaud Spiwack, 01/29/2014