- Make `flöb_pre` and `flöb` local to the proof.
- The metavariables `Ψ` are used for predicates, so use a `Q` here.