Add lemmas used by RefinedRust

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.