chore: update to lean4:v4.11.0-rc2

[tobiasgrosser]

Lean is now actively complaining about variable definitions that change theorem statements by only being references in proofs. Hence, we drop some widereaching variable definitions and inline them into the proofs.

There are still a small number of warnings that should be addressed, but the major changes are in this PR:

warning: ././././SSA/Core/ErasedContext.lean:344:0: included section variable '[TyDenote Ty]' is not used in 'Ctxt.Valuation.ofPair_fst', consider excluding it warning: ././././SSA/Core/ErasedContext.lean:347:0: included section variable '[TyDenote Ty]' is not used in 'Ctxt.Valuation.ofPair_snd', consider excluding it ⚠ [698/778] Replayed SSA.Core.Framework warning: ././././SSA/Core/Framework.lean:1528:8: included section variable '[DialectSignature d]' is not used in 'HVector.vars_nil', consider excluding it warning: ././././SSA/Core/Framework.lean:1532:8: included section variable '[DialectSignature d]' is not used in 'HVector.vars_cons', consider excluding it

I appreciate feedback on how this change is implemented and suggestions for improving our use of variables.