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
restate_axiom makes a new copy of a structure field, first definitionally simplifying the type.
This is useful to remove auto_param or opt_param from the statement.
As an example, we have:
structureA:=(x:ℕ)(a':x=1.skip)example(z:A):z.x=1:=byrwA.a'-- rewrite tactic failed, lemma is not an equality nor a iffrestate_axiomA.a'example(z:A):z.x=1:=byrwA.a
By default, restate_axiom names the new lemma by removing a trailing ', or otherwise appending
_lemma if there is no trailing '. You can also give restate_axiom a second argument to
specify the new name, as in