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)}eq:{T=
}, x,y,z:T. eq(x,y) eq(y,z) eq(x,z) (
f:{T=}. True) (f:(T
T
). x,y:T. f(x,y) 
x = y) Q == PQ
is mentioned by
| 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* eq:{T=}, x,y,z:T. eq(x,y) eq(y,z) eq(x,z) | [discrete_equality_transitive] |
| 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] |
In prior sections: core well fnd int 1 bool 1