1/1: Building eq (eq.idr)
Error: badeq x y p is not a valid impossible case.

eq.idr:27:1--27:23
    |
 27 | badeq x y p impossible
    | ^^^^^^^^^^^^^^^^^^^^^^

Error: badeqL xs ys p is not a valid impossible case.

eq.idr:30:1--30:26
    |
 30 | badeqL xs ys p impossible
    | ^^^^^^^^^^^^^^^^^^^^^^^^^