Who Cites discrete?
discrete	Def Discrete{T} == x,y:T. Dec(x = y)
	Thm* T:Type{i}. Discrete{T} Type{i'}
discrete_equality	Def {T=} == {eq:(TT)| x,y:T. (eq(x,y)) x = y }
	Thm* T:Type. {T=} Type
decidable	Def Dec(P) == P P
	Thm* A:Prop. Dec(A) Prop
assert	Def b == if b True else False fi
	Thm* b:. b Prop
iff	Def P Q == (P Q) & (P Q)
	Thm* A,B:Prop. (A B) Prop
not	Def A == A False
	Thm* A:Prop. (A) Prop
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop

About: