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.

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.
```

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.

What is `a`

?

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.

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

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

Last updated: Oct 04 2023 at 21:01 UTC