I have predicate `incl`

defined as

```
Definition incl (T : eqType) (vrs' vrs : seq T) := all (fun x => has (pred1 x) vrs) vrs'.
```

Now I would like to define it as

```
Definition incl (T : eqType) (vrs' vrs : seq T) := all (mem vrs) vrs'.
```

because it looks nicer to me (thanks to @Christian Doczkal for the hint).

The question.

When this lemma is defined using `has`

I can use `rewrite has_pred1 mem_undup`

like it is shown below

```
Lemma incl_undup (T : eqType) (vrs vrs' : seq T) : incl vrs (undup (vrs ++ vrs')).
move => vrs vrs'; rewrite /incl; apply/allP => t.
```

```
T : eqType
vrs, vrs' : seq T
t : T
============================
t \in vrs -> has (pred1 t) (undup (vrs ++ vrs'))
```

```
(* now rewrite *)
rewrite has_pred1 mem_undup mem_cat.
```

When it is defined with mem, I'm a bit stuck with rewrite step at this moment

```
T : eqType
vrs, vrs' : seq T
t : T
============================
t \in vrs -> mem (undup (vrs ++ vrs')) t
```

So, how to work with `mem`

in this case?

It is often a good idea to simplify (using `/=`

). In this case `mem _ _`

simplifies to `_ \in _`

and you can finish your proof with:

```
by rewrite /= mem_undup mem_cat => ->.
```

Great thanks!

Andrey Klaus has marked this topic as resolved.

Andrey Klaus has marked this topic as unresolved.

Andrey Klaus has marked this topic as resolved.

Last updated: Dec 06 2023 at 13:01 UTC