Is it possible to name the proofs written under a `Next Obligation`

?

E.g something like

```
Next Obligation as foo_proof
(* ... *)
Qed.
Print foo_proof.
```

Is it possible to name the proofs written under a `Next Obligation`

?

E.g something like

```
Next Obligation as foo_proof
(* ... *)
Qed.
Print foo_proof.
```

As far as I know, this is not possible. The proofs are automatically named though: in Equations, the scheme is “*foo*_obligations_obligation_*i*” (where *foo* is the name of the function, and *i* is the number of the obligation, and in Program it is simply “*foo*_obligation_*i*”.

But maybe if you tell us *what* you want to do with this named proof, we can find another way to achieve it?