set(build_proof_object). set(auto). list(usable). % NAME: reflexivity x = x. % NAME: commutativity x+y = y+x. % NAME: associativity (x+y)+z = x+y+z. % NAME: huntington n(x+n(y))+n(n(x)+n(y)) = y. % NAME: goal a+a != a. end_of_list.