Add an UnfoldOnce/delta_once normalizer step

[mtzguido]

Discussed with @nikswamy and @tahina-pro , motivated by #3616 from @TWal.

This adds a way to unfold a top-level definition, recursive or not, only 'once', avoiding any possible normalization loops. This PR also uses it for reveal_opaque, so it still works for recursive functions (after #3621) and will avoid unfolding loops. Here is the documentation for the step:

(** Like [delta_only], unfold only the definitions in this list,
but do so only once. This is useful for a controlled unfolding
of recursive definitions. NOTE: if there are many occurrences
of a variable in this list, it is unspecified which one will
be unfolded (currently it depends on normalization order). *)
val delta_once (s: list string) : Tot norm_step

Running a check here: https://github.com/mtzguido/FStar/actions/runs/12206414931