formula_list(usable). % third (and last) Huntington's axiom
	all x y ( u(c(u(c(x),y)),c(u(c(x),c(y)))) = x ). % BIII
end_of_list.