At:
filter is member lemma1111111111111122121
1.
T: Type
2.
eq: {T=}
3.
eq TT
4.
x,y:T. eq(x,y) x = y
5.
P: T
6.
x: T
7.
M: T List
8.
P(x)
9.
u: T
10.
v: T List
11.
x(eq) v x(eq) filter((x.P(x));v)
12.
eq(x,u) = true
13.
True
14.
P(u) = false
15.
x = u
x(eq) filter((x.P(x));v)
By:
FwdThru
Thm*P:. P P = false
[-2]
Generated subgoal:
P(u)
x(
eq) filter((
x.P(x));v)
}
T
x,y:T. eq(x,y) 
x = y
