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

At: is member filter lemma

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

11. T: Type
2. eq: {T=}
3. P: T
4. L: T List
5. x: T
6. x(eq) filter((x.P(x));L)
P(x)
21. T: Type{i}
2. eq: {T=}
3. P: T
4. L: T List
5. x: T
x(eq) filter((x.P(x));L) Prop{1}
31. T: Type
2. eq: {T=}
3. P: T
4. L: T List
T Type
41. T: Type
2. eq: {T=}
3. P: T
T List Type
51. T: Type
2. eq: {T=}
T Type
61. T: Type
{T=} Type
7 Type{i} Type{i'}

About:
listboolassertlambdafunctionuniversememberpropimpliesall

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