как назвать предположение при запоминании выражения?

Документация для Coq содержит общее предостережение , а не полагаться на встроенный механизм именования, а выбирать собственные имена, чтобы изменения в механизме именования не сделали прошлые доказательства недействительными.

При рассмотрении выражений вида remember Expr as vпеременной vприсваивается выражение Expr. Но имя предположения выбирается автоматически и имеет вид Heqv, так что имеем:

Heqv: v = Expr

Как я могу выбрать свое имя вместо Heqv? Я всегда могу переименовать его во что угодно, используя команду rename, но это не делает мои доказательства независимыми от гипотетических будущих изменений во встроенном механизме именования в Coq.