We introduce bisimulation up to congruence'' as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weakerbisimulation up to equivalence'' technique. The resulting algorithm can be exponentially faster than the recently introduced ``antichain algorithms''.