restate_axiom takes a structure field, and makes a new, definitionally simplified copy of it. If the existing field name ends with a ', the new field just has the prime removed. Otherwise, we append _lemma. The main application is to provide clean versions of structure fields that have been tagged with an auto_param.