|- ∀P f l. (∀p. P p ∧ f p > l ⇒ ∃p'. P p' ∧ f p' < f p) ⇒ ∀p. P p ⇒ ∃p'. P p' ∧ f p' ≤ l
|- ∀P f l prob. (∀p. P (prob,p) ∧ f p > l ⇒ ∃p'. P (prob,p') ∧ f p' < f p) ⇒ ∀p. P (prob,p) ⇒ ∃p'. P (prob,p') ∧ f p' ≤ l