At:
discrete list11221111
1.
T: Type
2.
Discrete{T}
3.
x: T List
4.
u: T
5.
v: T List
6.
y:T List. Dec(v = y)
7.
y: T List
8.
u1: T
9.
v1: T List
10.
u.v = v1
11.
u.v = [u1; u/ v]
False
By:
ApFunToHypEquands `L' (||(L)) 11
THEN
AbReduce -1
THEN
Inst
Thm*L:T List. ||(L)0
[T;v]
Generated subgoals:
y:T List. Dec(v = y)
False
|(L)) 
11
0
[T;v]