1)I have hypothesis that a exists in l . I should write it as (In a l or List.In a l)?

2) During induction i get In a [].This is wrong statement in the presence of hypothesis

(In a l). How to prove it wrong?

1) They are the same

```
Require Import List.
Import ListNotations.
Locate In.
Check In.
Check List.In.
Check Lists.List.In.
Check Coq.Lists.List.In.
```

```
```

2) There is a theorem `in_nil`

```
Require Import List.
Import ListNotations.
Check in_nil.
Goal forall (a : nat) (P : Prop), In a [] -> P.
Proof.
intros a P H.
Check (@in_nil _ a).
destruct (@in_nil _ a).
exact H.
Qed.
```

Last updated: Jun 18 2024 at 09:02 UTC