Bug in mcases

[valis]

The following code produces IllegalStateException:

\import Equiv
\import Function
\import Logic
\import Logic.Meta
\import Meta

\record Foo {
  | arr : Array (Fin 1) 2
  | allDiff : isInj arr
}

\func testFoo : Equiv {Foo} {Empty}
  => \new QEquiv {
    | f x => \case \elim x \with {
      | (a :: b :: nil, q) => \case \elim a, \elim b, \elim q \with {
        | 0, 0, q => contradiction (q {1} {0} idp)
      }
    }
    | ret => absurd
    | ret_f _ => mcases
    | f_sec => {?}
  }