formula_list(usable). % Robbins' variant of the third Huntington's axiom all x y ( c(u(c(u(x,y)),c(u(x,c(y))))) = x ). % BIII' end_of_list.