At:
is member equality strengthening lemma11111
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))
M,N:T List. L = (M @ (y.N))
By:
Witness M
THEN
Witness N
Generated subgoals:
}
equiv) L
M,N:T List. L = (M @ (y.N))