Steel effect: Assume requires clause when typechecking ensures

[R1kM]

Consider the following toy example, as reported by @cmovcc:

let test (x: nat)
  : Steel nat
  emp (fun _ -> emp)
  (requires (fun _ -> x > 0))
  (ensures (fun _ r _ -> r = 1 / x))
  =
  return (1 / x)

While the requires clause is in the logical context when typechecking (and verifying) the body of the function, it is not when typechecking the ensures clause itself. Hence,

val test (x: nat)
  : Steel nat
  emp (fun _ -> emp)
  (requires (fun _ -> x > 0))
  (ensures (fun _ r _ -> r = 1 / x))

currently fails to typecheck, because the prover cannot determine that x <> 0 in the ensures clause.

This PR addresses this issue by adopting a similar technique as other existing pure and stateful effects: the type of the ensures clause (Steel.Effect.Common.ens_t) now assumes the validity of the requires clause on the initial state.

Most of the PR consists of propagating this change to the different Steel effect combinators. There is also a minor tweak to the tactic in charge of rewriting frame equalities: Because of the new refinement on the type of the initial rmem state, a refinement subtyping SMT goal is generated during the call to rewrite_with_tactic. Unfortunately, rewrite_with_tactic fails when goals are remaining instead of passing them to SMT. This should probably be fixed, but in the meantime, the generated SMT goal is taken care of in the frame_vc_norm tactic.

Fixes #2435

[R1kM]

This fix unfortunately comes with a memory blowup leading to examples/steel/Queue failing for instance with an OOM error on the CI machine