Def pq == if p q else false fi

Thm* p,q:. (pq)

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