At:
is intersection implies exists element122111112
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.
xv.x(eq) M
9.
v(eq)M
10.
x: {x:T| x(eq) v }
11.
x(eq) M
12.
eq(x,u) = false
x(eq) v
By:
Analyze 10
THEN
UnhideSqStableHyp 11
Generated subgoals:
}
(eq)M 
(
x:{x:T| x(
eq) v }. x(
x(