If I `destruct`

a thing involving a `bool`

(or `remember`

a `bool`

), the resulting bool will most likely be called `b`

, `b0`

, `b1`

, …; a natural number will be `n`

, …; and so on. Can I access the same name generation mechanism from `Ltac`

? `fresh`

defaults to `H`

no matter what, I can only pass in a name or string (or several) to use in place of `H`

. What if I don’t have any?

The concrete context I currently want that in is writing a `remember`

variant that flips the equality. (Both `rewrite`

and most library theorems expect the equality to have the opposite direction from what `remember`

generates, and I don’t want to deal with using `rewrite <-`

or `symmetry in`

or whatever all. the. time.)

So far I have:

```
Tactic Notation "remember'" constr(t) "as" ident(x) "eqn" ":" ident(H) :=
(* NB: using "eqn:" instead of "eqn" ":" in the Notation messes up the grammar *)
remember t as x eqn:H; symmetry in H.
Tactic Notation "remember'" constr(t) "as" ident(x) :=
let H := fresh "Heq" x in remember' t as x eqn:H.
```

Now I’d also like to have a `Tactic Notation "remember'" constr(t) := …`

that makes nice names like `remember`

does, but I don’t know how to access the name generation mechanism. Any pointers?