Index notation cause internal exception

[lecopivo]

This code

import LeanColls.Classes.Indexed

open LeanColls

variable {Cont Idx Elem} [IndexType Idx] [Indexed Cont Idx Elem] [Inhabited Elem]

example (f : Idx → Elem) :
  Function.invFun (fun (f : Idx → Elem) => Indexed.ofFn (C:=Cont) f)
  =
  fun x i => x[i] := sorry

cause

internal exception: isDefEqStuck

I will investigate this as it is my doing.