```
H0 : In a [c']
H1 : In b [c']
```

a b c' are nat. May i have both above hypothesis at same time? When there is one element in the list then presence of

a and b in list is not possible.

You can have both if `a = b`

.

```
Require Import List.
Import ListNotations.
Check in_inv.
Check in_nil.
Goal forall (a b c : nat), In a [c] -> In b [c] -> a = b.
Proof.
intros a b c H0 H1.
destruct (in_inv H0) as [H2|H2].
- destruct (in_inv H1) as [H3|H3].
+ now rewrite <- H2.
+ now destruct (in_nil H3).
- now destruct (in_nil H2).
Qed.
```

Last updated: Oct 04 2023 at 23:01 UTC