[Agda] Solver usage

[Nils Anders Danielsson]

On 23/01/2019 12.29, Sergei Meshveliani wrote:
> Maybe the prover could be adopted to the case of
>            CommutativeRing  + the axiom of  0# ≉ 1# ?
> 
> Also, it looks like it fails to prove  x - x ≈ 0#,
> which can be derived from the Group instance for _+_.

I suggest that you study the paper by Grégoire and Mahboubi that I
linked to.

-- 
/NAD