Def i=j == if i=jtrue; false fi

Thm* i,j:. i=j

Def b == if b True else False fi

Thm* b:. b Prop

Def false ==

Thm* false

Def true ==

Thm* true

Def if b t else f fi == dec(b ; t; f)

Thm* b:, A:Type, p,q:A. if b p else q fi A