Agda-2.3.2.2: test/fail/Issue628.err
Issue628.agda:27,37-41 0 != 1 of type ℕ when checking that the expression refl has type 0 ≡ suc (divSucAux 0 0 0 1)
Issue628.agda:27,37-41 0 != 1 of type ℕ when checking that the expression refl has type 0 ≡ suc (divSucAux 0 0 0 1)