Def pq == p q

Thm* p,q:. pq

Def b == if b false else true fi

Thm* b:. b

Def p q == if p true else q fi

Thm* p,q:. (p q)

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