x,y:T. Dec(x = y)
Thm* T:Type{i}. Discrete{T} 
Type{i'}
P
Thm* A:Prop. Dec(A) Prop
A == A 
False
Thm* A:Prop. (A) Prop
| discrete |
Def Discrete{T} == x,y:T. Dec(x = y)
Thm* |
| decidable |
Def Dec(P) == P P
Thm* |
| not |
Def A == A False
Thm* |
About:
 |  |  |  |  |
 |  |  |  |