and_assoc: (all P:bool, Q:bool, R:bool. (P and Q and R) = (P and Q and R))

and_false: (all P:bool. (P and false) = false)

and_idempotent: (all P:bool. (P and P) = P)

and_or_absorb: (all P:bool, Q:bool. (P and (P or Q)) = P)

and_or_distrib: (all P:bool, Q:bool, R:bool. (P and (Q or R)) = ((P and Q) or (P and R)))

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

and_true: (all P:bool. (P and true) = P)

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)

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

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

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

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

iff_refl: (all P:bool. (P ⇔ P))

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)))

implies_refl: (all P:bool. (if P then P))

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

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

not_and: (all P:bool, Q:bool. (not (P and Q)) = (not P or not Q))

not_or: (all P:bool, Q:bool. (not (P or Q)) = (not P and not Q))

or_and_absorb: (all P:bool, Q:bool. (P or (P and Q)) = P)

or_and_distrib: (all P:bool, Q:bool, R:bool. (P or (Q and R)) = ((P or Q) and (P or R)))

or_assoc: (all P:bool, Q:bool, R:bool. (P or Q or R) = (P or Q or R))

or_false: (all P:bool. (P or false) = P)

or_idempotent: (all P:bool. (P or P) = P)

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

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

or_true: (all P:bool. (P or true) = true)

define xor : (fn (bool, bool) -> bool) = fun x:bool, y:bool {
      if x then
        not y
      else
        y
    }

xor_assoc: (all a:bool, b:bool, c:bool. xor(a, xor(b, c)) = xor(xor(a, b), c))

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

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

xor_neg: (all a:bool. xor(a, not a) = true)

xor_self: (all a:bool. xor(a, a) = false)

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