## Stream: Coq users

### Topic: Proofs on filters (ssreflect.seq)

#### Felipe Lisboa Malaquias (Aug 16 2021 at 12:38):

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

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.