Make `cong` more flexible.

It is now possible to skip a prefix of the arguments if they are already the same on both sides. This is intended to future-proof the format for support of partial application.