reveal_opaque doesn't work with recursive functions

[TWal]

Here is a problem, and a proposed fix (but I'm not sure which is the best option, hence I am not doing a PR directly).

In DY* we hide a a lot of functions, some of which are recursive.
Unfortunately, reveal_opaque doesn't work with such functions, as illustrated below

[@@"opaque_to_smt"]
let f (): int = 0

// the SMT cannot inspect the definition of `f`
[@@expect_failure]
let _ =
  assert(f () == 0)

// but we can reveal it
let _ =
  reveal_opaque (`%f) (f);
  assert(f () == 0)

// however if `f` is defined via `let rec`
[@@"opaque_to_smt"]
let rec f_rec (): int = 0

// then `reveal_opaque` doesn't help!
[@@expect_failure]
let _ =
  reveal_opaque (`%f_rec) (f_rec);
  assert(f_rec () == 0)

One solution we use is to use the reveal_rec_opaque defined below (although we use norm_spec directly)

// with the `zeta` normalization rule
let reveal_rec_opaque (s: string) = norm_spec [delta_only [s]; zeta]

// then we can reveal the definition of `f_rec`
let _ =
  reveal_rec_opaque (`%f_rec) (f_rec);
  assert(f_rec () == 0)

Or we use normalize_term_spec when we are lazy, but this can reveal anything to the SMT so I wouldn't call it good practice.

Should we add reveal_rec_opaque in ulib? Or should we add the zeta rule in reveal_opaque directly to avoid dealing with two separate functions?