Def b == if b false else true fi

Thm* b:. b

Def pq == if p q else false fi

Thm* p,q:. (pq)

Def p q == if p true else q fi

Thm* p,q:. (p q)

Def == Unit+Unit

Thm* Type

Def true ==

Thm* true

Def false ==

Thm* false

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