prefer Context_Position.report_generic, which observes is_visible flag and thus reduces number of echos;

clarified signature;

avoid spurious warning in invisible context, notably Haftmann-Wenzel sandwich;

made Context_Position independent from Config;

use Nitpick as an oracle for finite problems

add extensionality to first-order provers

avoid duplicate helpers

mention tools and packages earlier;

tuned;

tuned;