The Coq mailing list

[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