Def p=q == (pq) (pq)

Thm* p,q:. p=q

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)