At:
discrete list
1
1
2
1
1
1
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.
u.v = nil
False
By:
ApFunToHypEquands `L' (|
|(L)) 
8
THEN
AbReduce -1
THEN
Inst
Thm* L:T List. ||(L)
0
[T;v]
Generated subgoals:
None
About:
