A counter-example finder for higher-order logic, designed to be used from various proof assistants