Issue431.agda:16,25-29
Refusing to invert pattern matching of double because the maximum
depth (10) has been reached. Most likely this means you have an
unsatisfiable constraint, but it could also mean that you need to
increase the maximum depth using the flag --inversion-max-depth=N
when checking that the expression refl has type
double (suc (suc (suc (suc (suc _19))))) ≡
suc (double (suc (suc (suc (suc _18)))))
Failed to solve the following constraints:
  _20 := refl [blocked on problem 22]
  [22, 26, 28, 30, 32, 34, 36, 38, 40, 42, 44] double _18
                                                 = suc (double _19)
                                                 : Nat
Unsolved metas at the following locations:
  Issue431.agda:16,25-29
