A helper function that can be useful to implement enforce, in particular in sharing a default logic for blang constructors that cannot be automatically enforced.

Returns the list of elements from the input condition that are directly reachable as elements to be enforced, without going through dynamic conditions or SAT logic. In practice, that is Base, and elements under And _ recursively.

A helper that applies some usually helpful heuristic when proposing a new name based on the `is_prefix predicate. Assumed to be called when the given prefix is not already a prefix of the input, otherwise the output is unspecified.