T1:Type{i}, T2:Type{j}. Discrete{T1} 
Discrete{T2} Discrete{(T1
T2)}T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1+T2)} (
f:{T=
}. True) (f:(T
T
). x,y:T. f(x,y) 
x = y)x,y:T. Dec(x = y)
is mentioned by
| Thm* Discrete{Atom} | [discrete__atom] |
| Thm* T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1T2)} | [discrete__product] |
| Thm* T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1+T2)} | [discrete__union] |
| Thm* Discrete{T} (f:{T=}. True) | [discrete_implies_discrete_equality] |
| Thm* Discrete{T} (f:(TT). x,y:T. f(x,y) x = y) | [discrete_implies_bool_equality] |