Hey, beginner question here.

I'm trying to prove a Lemma containing some hypotheses and a goal that look like this:

```
x : Type_t
R : seq Type_t
H : x \in [seq elem <- R | elem.(field) == value]
------------------------------------------------------------
x.(field) == value
```

Whereas Type_t ia an eqType Record defined by me.

How could I assert that the predicate used on the filter function is true ? If I can assert such thing, applying the Lemma below might solve my issue.

filter_predT: forall [T : Type] (s : seq T), [seq x <- s | predT x] = s

Thanks in advance,

You should be able to do a `move: H; rewrite mem_filter`

to get `x \in R`

and `x.(field) == value`

. The lemma `filter_predT`

is for eliminating a trivial filter, which yours does not seem to be. Hope this helps.

Last updated: Jun 13 2024 at 06:01 UTC