coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Symmetry does not work with <>

From: Marcus Ramos <marcus.ramos AT univasf.edu.br>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Symmetry does not work with <>
Date: Tue, 22 Jul 2014 17:59:33 -0300

Thanks a lot.

Marcus.

2014-07-22 17:53 GMT-03:00 Jonathan <jonikelee AT gmail.com>:

On 07/22/2014 04:46 PM, Marcus Ramos wrote:

Hi,

My goal is "l <> []", however I need it to be "[] <> l". How can I get
this since symmetry does not work for <>?

Thanks,
Marcus.

intro H; symmetry in H; contradict H.

Or, apply the lemma not_eq_sym:

not_eq_sym: forall (A : Type) (x y : A), x <> y -> y <> x

-- Jonathan

[Coq-Club] Symmetry does not work with <>, Marcus Ramos, 07/22/2014
- Re: [Coq-Club] Symmetry does not work with <>, Jonathan, 07/22/2014
  - Re: [Coq-Club] Symmetry does not work with <>, Marcus Ramos, 07/22/2014
- Re: [Coq-Club] Symmetry does not work with <>, gallais, 07/23/2014
  - Re: [Coq-Club] Symmetry does not work with <>, Marcus Ramos, 07/28/2014