Who Cites equivalence?
equivalence	Def {T} == {f:(TT)| (x:T. (f(x,x))) & (x,y:T. (f(x,y)) (f(y,x))) & (x,y,z:T. (f(x,y)) (f(y,z)) (f(x,z))) }
	Thm* T:Type{i}. {T} Type{i'}
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
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop

Syntax:

{T}

has structure:

equivalence(T)

About: