feat: add lifting and ectx lifting

[ayhon]

Description

Ports lifting.v and ectx-lifting.v.

Fixes #348 and #349.

Builds on top of #393.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[markusdemedeiros]

This looks pretty good, is it ready to review?

[ayhon]

Yes, I have also gone over the comments I received in my last PR and made changes based on that, so hopefully there won't be much to change (famous last words).

[markusdemedeiros]

Super! On it

[markusdemedeiros]

Beauty :) Thanks for putting in the effort to make your PR quick to review. Aside from a couple style cleanups, the only major change was accepting your proposal to use ∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v instead of Option.rec. I suspect the reason they do this in Rocq is to have a form which automatically reduces better in some contexts, but we will try this way since it is cleaner and I suspect pretty easy for us to automate anyways.

[ayhon]

Cool! I think there's a couple more changes I'd like to make in BI/Updates.lean. I recently introduced a step_fupd_mono lemma which was not present in Rocq which might simplify many of our instances of mono <| later_mono <| mono ?_ in the code

EDIT: Well, we can add those in some other PR

[markusdemedeiros]

Sounds good. If you explore this further please make another PR.

[ayhon]

I opened #404. Warning, it's quite a minor PR