At:
discrete list1122211211111
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.
(Case of u.v; nil nil ; h.t t) = (Case of u1.v1; nil nil ; h.t t) T List
False
u.v = v1
T
u = u1
nil ; h.t 
T List
