At:
discrete list112221121211
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
False
By:
ApFunToHypEquands `L' (Case of L; nil u ; h.t h) T 14
Generated subgoal:
u ; h.t 
False
u.v = v1
T
u = u1
