Defining invariant that CachedAnalysis must hold, update PrecondElim

[aqjune-aws]

Once PrecondElim is updated, we can make #687 use FilterProcedure too.

[MikaelMayer]

🤖 Autopilot is stuck on comments after 2 attempts with no progress. Needs human help.

[MikaelMayer]

🤖 Autopilot started working on this (branch issue-702-defining-invariant-that-cachedanalysis-m)