(41steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: filter is member lemma


T:Type, eq:{T=}, P:(T), L:T List, x:T. x(eq) L P(x) x(eq) filter((x.P(x));L)

By: UnivCD

Generated subgoal:

11. T: Type
2. eq: {T=}
3. P: T
4. L: T List
5. x: T
6. x(eq) L
7. P(x)
x(eq) filter((x.P(x));L)

About:
listboolassertlambdafunctionuniverseimpliesall

(41steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc