Fix #3616

[mtzguido]

Taking the suggestion from @TWal of adding zeta to the steps in reveal_opaque.

Note, this can cause issues when the function being revealed is recursive and not guarded by a pattern match. E.g.

let f () : Dv int = f ()

This will send the normalizer into a loop which will stack overflow. I don't think these are usual occurrences and this is a separate problem of the normalizer itself, so I think adding zeta is not too bad. When the recursion is under a match (almost always) this will block the unfolding and work OK.

[mtzguido]

https://github.com/mtzguido/FStar/actions/runs/12165596509