coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove that inductive substructures are not equal?

From: Michiel Helvensteijn <mhelvens AT gmail.com>
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to prove that inductive substructures are not equal?
Date: Mon, 15 Jul 2013 15:59:45 +0200

On Mon, Jul 15, 2013 at 3:15 PM, Viktor Vafeiadis
<viktor AT mpi-sws.org>
wrote:
> induction t; congruence.

On Mon, Jul 15, 2013 at 3:19 PM, Adam Chlipala
<adamc AT csail.mit.edu>
wrote:
> Generally this work is easy to push off onto [congruence], which is a
> complete decision procedure for equality with constructors.

Thanks both!

--
www.mhelvens.net

[Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
  - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
  - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
    - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Adam Chlipala, 07/15/2013
      - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
      - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Cedric Auger, 07/15/2013
        
        Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013
    - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Cedric Auger, 07/15/2013
      - Re: [Coq-Club] How to prove that inductive substructures are not equal?, Michiel Helvensteijn, 07/15/2013