Discrete{(T List)}
L:T List. |
|(L)
0 (
f:(T
T
). x,y:T. f(x,y) 
x = y)| Theorem | Name | ||
| Thm* Discrete{T} Discrete{(T List)} | [discrete__list] | ||
| cites | |||
| Thm* L:T List. ||(L)0 | [list_length_non_negative] | ||
| Thm* Discrete{T} (f:(TT). x,y:T. f(x,y) x = y) | [discrete_implies_bool_equality] |