Def p = q == if p q else q fi

Thm* p,q:. p = q

Def P Q == (P Q) & (P Q)

Thm* A,B:Prop. (A B) Prop

Def b == if b false else true fi

Thm* b:. b

Def P Q == Q P

Thm* A,B:Prop. (A B) Prop