[prover] Aggregated behavioral-predicate assumes use a single pre-label per callee

[wrwg]

For tracking. See TODO(#...) in spec_instrumentation.rs (find_behavior_pre_label_for_callee).