Collect #Ceil conditions introduced by equations with partial functions

While runtimeverification/haskell-backend#3779 is concerned with rewrite rules (and relatively straightforward), collecting #Ceil conditions introduced by simplifications and function-defining equations is complex because of

• possible recursive evaluation of side conditions - the collected #Ceil conditions may have to be discarded if the recursive caller ends up failing for other reasons
• when the #Ceil condition comes from simplifying a rewrite rule side condition, the negated condition becomes a remainder and rewriting needs to proceed with this remainder added to the assumed condition (unless it can be pruned - has to be simplified "soon"). This potentially leads to branching.

This extension is expected to considerably reduce the fall-back cases because many more simplifications can be applied.

The issue names no files, tests, or entry points. Read runtimeverification/haskell-backend#3779 first for the related rewrite-rule work, then trace how simplifications and function-defining equations collect #Ceil conditions. Done means the recursive, branching cases and fallback reduction described here are handled without retaining invalid conditions.