Quasigroup solver benchmark

Adds a backtracking solver for the quasigroup completion problem as a benchmark.

The solver makes somewhat heavy use of dependent typing to statically verify the correctness of solutions produced.