Selected Objects
| def | discrete | Discrete{T} ==  x,y:T. Dec(x = y) |
| THM | discrete_implies_bool_equality | Discrete{T}   ( f:(T  T ). x,y:T. f(x,y)  x = y) |
| def | discrete_equality | {T= } == {eq:(TT)| x,y:T. eq(x,y) x = y } |
| THM | discrete_equality_inc | {T=}  (TT) |
| THM | discrete_equality_properties | eq:{T=}. (x,y:T. eq(x,y) x = y) & eq  TT |
| THM | discrete_implies_discrete_equality | Discrete{T} (f:{T=}. True) |
| THM | discrete_equality_unique | f1,f2:{T=}. f1 = f2 TT |
| THM | discrete_equality_reflexive | eq:{T=}, u:T. eq(u,u) |
| THM | discrete_equality_symmetric | eq:{T=}, x,y:T. eq(x,y) eq(y,x) |
| THM | discrete_equality_transitive | eq:{T=}, x,y,z:T. eq(x,y) eq(y,z) eq(x,z) |
| THM | discrete__union | T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1+T2)} |
| THM | discrete__product | T1:Type{i}, T2:Type{j}. Discrete{T1} Discrete{T2} Discrete{(T1 T2)} |
| THM | discrete__atom | Discrete{Atom} |