The proof just plugs together the information in the hypotheses. The only external things we need are

• downward closure of P, to get from P f to P g
• transitivity of <= (aka downward closure of bounding)

Next: accumulating a unifier | Prev: the optimist's theorem | Up: contents