At:
is member equality strengthening lemma11112
1.
T: Type
2.
equiv: {T}
3.
eq: {T=}
4.
u: T
5.
L: T List
6.
u(equiv) L
7.
M: T List
8.
N: T List
9.
y: T
10.
equiv(u,y)
11.
L = (M @ (y.N))
12.
y(eq) L
v:T. equiv(u,v) & v(eq) L
By:
Analyze 3
THEN
Analyze 2
THEN
Witness y
Generated subgoals:
}
equiv) L
v:T. equiv(u,v) & v(