how to name the assumption when remembering an expression?

Viewed 415

The documentation for Coq carries the general admonition not to rely on the builtin naming mechanism, but select one's own names, lest the changes in the naming mechanism render past proofs invalid.

When considering expressions of the form remember Expr as v, we set the variable v to the expression Expr. But the name of the assumption is selected automatically, and is something like Heqv, so we have:

Heqv: v = Expr

How can I select my own name instead of Heqv? I can always rename it to whatever I like using the rename command, but that doesn't keep my proofs independent of the hypothetical future changes in the builtin naming mechanism in Coq.

1 Answers
Related