This MR adds lemmas that RefinedRust uses in its model of lifetime contexts.
Since the lifetime logic is now a separate opam package, this would allow us to use that package instead of maintaining a fork of lambda-rust.