At:
is intersection implies exists element
1
2
1
1
1
1
1.
T: Type
2.
eq: {T=
}
3.
L: T List
4.
M: T List
5.
u: T
6.
v: T List
7.
v
(eq)M 
(
x:{x:T| x(
eq) v }. x(eq) M)
8.
u(eq) M
eq(u,u) = true
By:
BackThru
Thm* 
P:
. P 
P = true
Generated subgoal:
| 1 | eq(u,u) |
About:
