I'm not able to find such lemma. So, the question, do I miss something or there is no such lemma yet?

So, I need to proof lemmas as next

```
Lemma mem_head' (T : eqType) (x a : T) s : x \in s -> x \in (a :: s). Admitted.
Lemma mem_cat_fst (T : eqType) (x : T) s' : forall s, x \in s -> x \in (s ++ s'). Admitted.
Lemma mem_cat_snd (T : eqType) (x : T) s : forall s', x \in s -> x \in (s ++ s'). Admitted.
```

Hi @Andrey Klaus , indeed there should be such a lemma, one sec

You have `in_cons`

and `mem_cat`

So to prove that you use a bit different proof style

```
by move=> x_in_s; rewrite mem_cat x_in_s.
```

Hello, Emilio! Thank you very much! Especially for the proof style hint.

The reason this style is preferred is that math-comp defaults to rewriting lemmas (as they tend to work a bit more generally) when an equational theory exists

Note how mem_cat goes in both directions, so it is a bit more "general"

Note also that `in_cons`

is usually a part of the `inE`

rewriting db

it is a good idea to extend inE (locally) for your own needs, but beware of performance

You are most welcome

One point of using equations is that they work the same, no matter whether you're rewriting in an assumption or in the conclusion. Also, they often allow proving additional equalities without making any case analysis, as seen by the following (contrived) example:

```
Goal forall (T: eqType) (s : seq T) x, (x \in s ++ s) = (x \in s).
Proof. by move=> T s x; rewrite mem_cat orbb. Qed.
```

Note that there is no need to make this a lemma, because one can simulate rewriting with this lemmas by rewriting with `mem_cat`

and `orbb`

. So another benefit is that one needs fewer lemmas.

@Christian Doczkal , thank you very much for the explanation. I can see now why there is no such lemmas.

Andrey Klaus has marked this topic as resolved.

Last updated: Jan 29 2023 at 19:02 UTC