(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:
1
1.
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:
(41steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc