At:
discrete list11222112121111
1.
T: Type
2.
Discrete{T}
3.
x: T List
4.
u: T
5.
v: T List
6.
y: T List
7.
u1: T
8.
v1: T List
9.
u.v = v1
10.
v = v1
11.
f: TT
12.
f(u,u1) u = u1
13.
f(u,u1)
14.
u.v = u1.v1
15.
u = u1
False
By:
Analyze 13
THEN
HypBackchain
Generated subgoals:
u.v = v1
T
u = u1
False