## Stream: Coq users

### Topic: no similarity

#### pianke (Apr 08 2023 at 11:28):

I want to add a constraint on natural number list that no element is repeated in the list. To solve the lemma related to this list how i should add this in hypothesis(no duplication) .I have a list c1::c2::t & H1:d1=c1 H2: d2=c2 . When i compare two elements of list then i could be able to derive beq_nat c1 c2=false.

#### Pierre Castéran (Apr 08 2023 at 12:02):

You may apply the following lemma:

``````Require Import List .

Lemma NoDup_xy_inv:  forall x y (l: list nat), NoDup (x::y::l) -> x <> y.
Proof.
intros x y l H Heq; inversion_clear H; subst;  apply H0; now constructor.
Qed.
``````

#### pianke (Apr 09 2023 at 06:30):

H1: l<>nil
H2: NoDup l=true or H2: NoDup (a::l)=true
I mean in hypothesis write it as above. To avoid the cases of repeation.

#### Laurent Théry (Apr 09 2023 at 07:30):

What is `a`?

#### Pierre Castéran (Apr 09 2023 at 09:41):

Looks to be some confusion between propositions and Booleans in your statements of `H2`. If you use Standard library’s `Nodup`, `NoDup l` is not a Boolean, but a proposition.

#### pianke (Apr 11 2023 at 03:06):

After induction on l, a is the first element of l.

#### Laurent Théry (Apr 11 2023 at 12:04):

so why you don't give us exactly the goal you have?

Last updated: Oct 04 2023 at 21:01 UTC