or_not: (all P:bool, Q:bool. (if ((P or Q) and not P) then Q))

ex_mid: (all b:bool. (b or not b))

or_sym: (all P:bool, Q:bool. (P or Q) = (Q or P))

and_sym: (all P:bool, Q:bool. (P and Q) = (Q and P))

eq_true: (all P:bool. (P ⇔ (P = true)))

eq_false: (all P:bool. (not P ⇔ (P = false)))

iff_equal: (all P:bool, Q:bool. (if (P ⇔ Q) then P = Q))

iff_symm: (all P:bool, Q:bool. (if (P ⇔ Q) then (Q ⇔ P)))

iff_trans: (all P:bool, Q:bool, R:bool. (if ((P ⇔ Q) and (Q ⇔ R)) then (P ⇔ R)))

contrapositive: (all P:bool, Q:bool. (if ((if P then Q) and not Q) then not P))

double_neg: (all P:bool. not not P = P)

fun xor(x:bool, y:bool) {
  if x then
    not y
  else
    y
}

xor_true: (all b:bool. xor(true, b) = not b)

xor_false: (all b:bool. xor(false, b) = b)

xor_commute: (all a:bool, b:bool. xor(a, b) = xor(b, a))