Redefined "Extract" to mean forall x. f x -> x, which makes more sense.