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?