Конгруэнтность для гетерогенного равенства

Я пытаюсь использовать гетерогенное равенство, чтобы доказать утверждения, содержащие этот индексированный тип данных:

data Counter : ℕ → Set where
  cut : (i j : ℕ) → Counter (suc i + j)

Я смог написать свои доказательства, используя RelationBinary.HeterogenousEquality.≅- Рассуждение , но только при условии следующего свойства конгруэнтности:

Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
               {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
               k ≅ k′ → f k ≅ f k′
Counter-cong f k≅k′ = {!!}

Однако я не могу сопоставить шаблон для k≅k ′ , являющегося refl , без получения следующего сообщения об ошибке из средства проверки типов:

Refuse to solve heterogeneous constraint 
    k : Counter n =?= k′ : Counter n′

и если я попытаюсь провести анализ случая на k≅k ′ (т.е. используя Cc Cc из внешнего интерфейса Emacs), чтобы убедиться, что все неявные аргументы должным образом сопоставлены с их ограничениями, налагаемыми refl , я получаю

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the 
inferred indices 
    [{.Level.zero}, {Counter n}, k] 
with the expected indices 
    [{.Level.zero}, {Counter n′}, k′]

(если вам интересно, вот несколько нерелевантных backgr ound: Удаление подстановки для доказательства равенства )